[isabelle-dev] Feature suggestion: apply (meth[1!])
makarius at sketis.net
Mon Mar 11 19:36:30 CET 2013
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.
More information about the isabelle-dev