src/Doc/JEdit/JEdit.thy
changeset 64549 964ac7439a52
parent 64515 29f0b8d2f952
child 64602 8edca3465758
equal deleted inserted replaced
64548:8b187a7a9776 64549:964ac7439a52
   721     "jedit_script_indent"} and @{system_option_def
   721     "jedit_script_indent"} and @{system_option_def
   722     "jedit_script_indent_limit"}.
   722     "jedit_script_indent_limit"}.
   723 
   723 
   724   The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
   724   The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
   725   Isabelle / General\<close>.
   725   Isabelle / General\<close>.
       
   726 
       
   727   \<^medskip> Automatic indentation has a tendency to produce trailing whitespace. That
       
   728   can be purged manually with the jEdit action @{action "remove-trailing-ws"}
       
   729   (shortcut \<^verbatim>\<open>C+e r\<close>). Moreover, the \<^emph>\<open>WhiteSpace\<close> plugin provides some
       
   730   aggressive options to trim whitespace on buffer-save.
   726 \<close>
   731 \<close>
   727 
   732 
   728 
   733 
   729 section \<open>SideKick parsers \label{sec:sidekick}\<close>
   734 section \<open>SideKick parsers \label{sec:sidekick}\<close>
   730 
   735