more on "Indentation";
authorwenzelm
Sun Nov 20 20:58:33 2016 +0100 (2016-11-20)
changeset 6451529f0b8d2f952
parent 64514 27914a4f8c70
child 64516 2c45b7af9173
more on "Indentation";
src/Doc/JEdit/JEdit.thy
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Sun Nov 20 20:12:42 2016 +0100
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Sun Nov 20 20:58:33 2016 +0100
     1.3 @@ -696,6 +696,36 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 +section \<open>Indentation\<close>
     1.8 +
     1.9 +text \<open>
    1.10 +  Isabelle/jEdit augments the existing indentation facilities of jEdit to take
    1.11 +  the structure of theory and proof texts into account. There is also special
    1.12 +  support for unstructured proof scripts.
    1.13 +
    1.14 +    \<^descr>[Syntactic indentation] follows the outer syntax of Isabelle/Isar.
    1.15 +
    1.16 +    Action @{action "indent-lines"} (shortcut \<^verbatim>\<open>C+i\<close>) indents the current line
    1.17 +    according to command keywords and some command substructure: this
    1.18 +    approximation may need further manual tuning.
    1.19 +
    1.20 +    Action @{action "isabelle.newline"} (shortcut \<^verbatim>\<open>ENTER\<close>) indents the old
    1.21 +    and the new line according to command keywords only: this leads to precise
    1.22 +    alignment of the main Isar language elements. This depends on option
    1.23 +    @{system_option_def "jedit_indent_newline"} (enabled by default).
    1.24 +
    1.25 +    \<^descr>[Semantic indentation] adds additional white space to unstructured proof
    1.26 +    scripts (\<^theory_text>\<open>apply\<close> etc.) via number of subgoals. This requires information
    1.27 +    of ongoing document processing and may thus lag behind, when the user is
    1.28 +    editing too quickly; see also option @{system_option_def
    1.29 +    "jedit_script_indent"} and @{system_option_def
    1.30 +    "jedit_script_indent_limit"}.
    1.31 +
    1.32 +  The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
    1.33 +  Isabelle / General\<close>.
    1.34 +\<close>
    1.35 +
    1.36 +
    1.37  section \<open>SideKick parsers \label{sec:sidekick}\<close>
    1.38  
    1.39  text \<open>