src/Doc/JEdit/JEdit.thy
changeset 66681 0879f2045965
parent 66574 e16b27bd3f76
child 66683 01189e46dc55
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Tue Sep 19 14:26:25 2017 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu Sep 21 10:58:34 2017 +0200
     1.3 @@ -720,6 +720,10 @@
     1.4      alignment of the main Isar language elements. This depends on option
     1.5      @{system_option_def "jedit_indent_newline"} (enabled by default).
     1.6  
     1.7 +    Regular input (via keyboard or completion) indents the current line
     1.8 +    whenever an new keyword is emerging the start of the line. This depends on
     1.9 +    option @{system_option_def "jedit_indent_input"} (enabled by default).
    1.10 +
    1.11      \<^descr>[Semantic indentation] adds additional white space to unstructured proof
    1.12      scripts (\<^theory_text>\<open>apply\<close> etc.) via number of subgoals. This requires information
    1.13      of ongoing document processing and may thus lag behind, when the user is
    1.14 @@ -728,12 +732,9 @@
    1.15      "jedit_script_indent_limit"}.
    1.16  
    1.17    The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
    1.18 -  Isabelle / General\<close>.
    1.19 -
    1.20 -  \<^medskip> Automatic indentation has a tendency to produce trailing whitespace. That
    1.21 -  can be purged manually with the jEdit action @{action "remove-trailing-ws"}
    1.22 -  (shortcut \<^verbatim>\<open>C+e r\<close>). Moreover, the \<^emph>\<open>WhiteSpace\<close> plugin provides some
    1.23 -  aggressive options to trim whitespace on buffer-save.
    1.24 +  Isabelle / General\<close>. A prerequisite for advanced indentation is \<^emph>\<open>Utilities
    1.25 +  / Buffer Options / Automatic indentation\<close>: it needs to be set to \<^verbatim>\<open>full\<close>
    1.26 +  (default).
    1.27  \<close>
    1.28  
    1.29