On 15/07/16 11:49, Lawrence Paulson wrote:
> It’s great, but can I pester you about my pet wish? It would be some sort of
> “auto-complete” e.g. I type “proof (cases blah)” and somehow automatically
> the full “case True show … next case False show … qed” skeleton could be
> generated? The same
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)
This is the updated situation according to Isabelle/019856db2bb6:
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Improved support for indentation according to Isabelle outer syntax.
Action "indent-lines" (shortcut C+i) indents the current line according
to command keywords and some command
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Indentation according to Isabelle outer syntax, cf. action
"indent-lines" (shortcut C+i).
This refers to Isabelle/52349e41d5dc.
It is only the second round of refinement, beyond direct imitation of
the old proof-indent.el from Proof General (see
