Re: [isabelle] Proof mode maintained after outcommenting [Re: Isabelle2012-RC3 available for testing]



Am 21/05/2012 09:45, schrieb Lars Noschinski:
> Now, if I input 'term "x', give it time to reparse and just then add the closing
> '"', the definition of K33 is not parsed anymore. And if I am in such a
> situation, the incremental reparsing goes wrong every few minutes.
> 
> (The cut-and-repaste workaround is non-disruptive enough that I am fine with it.
> If the only workaround I knew would be reloading (and thus reproving and losing
> Undo and a lot of time), I would probably switch back to Proof General).

I am afraid I was in this situation earlier on and I just gave up on jedit. The
theory was small, so it was not a question of cut-and-paste vs reload, but my
workflow was seriously disrupted by having to do something special every few
minutes to make jedit happy. It is also confusing to novices because you keep
staring at your text thinking there is something wrong with it although there isn't.

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.