[isabelle-dev] NEWS:

Makarius makarius at sketis.net
Thu Jul 21 12:09:50 CEST 2016

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Completion templates for commands involving "begin ... end" blocks,
e.g. 'context', 'notepad'.

This refers to Isabelle/0f39f59317c1. It can be seen as part of the
standardized indenation policy, although only line breaks without extra
indentation are involved here: the standard column is 0.

At some point, fold handling and maybe Sidekick should take "begin ...
end" blocks into account as well.


More information about the isabelle-dev mailing list