notes on whitespace;
authorwenzelm
Tue Dec 06 17:38:46 2016 +0100 (22 months ago)
changeset 64549964ac7439a52
parent 64548 8b187a7a9776
child 64550 3e20defb1e3c
notes on whitespace;
src/Doc/JEdit/JEdit.thy
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Tue Dec 06 17:23:54 2016 +0100
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Tue Dec 06 17:38:46 2016 +0100
     1.3 @@ -723,6 +723,11 @@
     1.4  
     1.5    The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
     1.6    Isabelle / General\<close>.
     1.7 +
     1.8 +  \<^medskip> Automatic indentation has a tendency to produce trailing whitespace. That
     1.9 +  can be purged manually with the jEdit action @{action "remove-trailing-ws"}
    1.10 +  (shortcut \<^verbatim>\<open>C+e r\<close>). Moreover, the \<^emph>\<open>WhiteSpace\<close> plugin provides some
    1.11 +  aggressive options to trim whitespace on buffer-save.
    1.12  \<close>
    1.13  
    1.14