This is another update according (presently at Isabelle/2033a3960c36):
* Syntactic indentation according to Isabelle outer syntax. Action
"indent-lines" (shortcut C+i) indents the current line according to
command keywords and some command substructure. Action
"isabelle.newline" (shortcut ENTER) indents the old and the new line
according to command keywords only; see also option
"jedit_indent_newline".
* Semantic indentation for unstructured proof scripts ('apply' etc.) via
number of subgoals. This requires information of ongoing document
processing and may thus lag behind, when the user is editing too
quickly; see also option "jedit_script_indent" and
"jedit_script_indent_limit".
There are a few more changes that are not described in the NEWS,
concerning 'begin' and quasi-commands like 'imports', 'fixes',
'assumes', 'shows', 'where'.
After mapping the ENTER key to "isabelle.newline", which needs to be
done manually, Isar source can be easily formatted nicely, often
requiring only one hand.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
