[isabelle-dev] NEWS: Indentation according to Isabelle outer syntax

[Makarius]

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 for induction? I know this is far from easy, given the amount of contextual information involved.

It is probably rather trivial. I will come back to variations on
sendback information eventually. One reason it was not done very often
so far is rather profane: lack of indentation for the inserted text.


	Makarius