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

[Lars Noschinski]

On 11.03.2013 17:51, Makarius wrote:
> This looks just like making the meaning of indentation a bit more
> formal. Lets say as a mode of checking in the Prover IDE: fail if
> something is wrong in that respect, or paint things in funny colors.

We shortly thought about this earlier and it has the appeal of 
formalizing an already established convention, which is definitely 
useful. However, there are two things which make me slightly 
uncomfortable with this solution:

   - when I'm exploring a proof which I expect to collapse into a
     one-line by-statement I usually don't (and don't want to) bother
     with indentation (this is obviously less of issue when using funny
     colors).

   - Isabelle does not have significant whitespace anywhere else (I'm
     aware of). It does not even consider linebreaks to be relevant. So
     my initial feeling about this suggestion is "neat hack".

> 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?

   -- Lars