[isabelle-dev] Feature suggestion: apply (meth[1!])

[Makarius]

On Mon, 11 Mar 2013, Lars Noschinski wrote:

>> Markup.proof_state is there for a long time already, to turn it into
>> some use.
>
> Does this mean this could be implemented exclusively on the jEdit side, 
> without touching the prover?

It depends what "this" actually shall mean here.  There is always some 
interplay of both Isabelle/ML and Isabelle/Scale to be expected, though.

Recently I have occasionally revisited the old question of indentation, 
mainly for structured proofs.  This is particularly relevant for editing 
partial (structurally broken) proof texts, and getting somehow "expected" 
errors, not just a red bloodshed over some odd script.


 	Makarius