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



Am 22/05/2012 10:46, schrieb Makarius:
> On Tue, 22 May 2012, Tobias Nipkow wrote:
> 
>>> (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 quality of the result critically depends on feedback by
> early adopters, not silently giving things up.

I don't think my email was silent, or was it? It was the direct reaction to a
jedit session. And to clarify what I said: I gave up on jedit for that session,
not for good. I have no doubt that these problems can be surmounted.

> So far I've often had the impression that many peoples don't want to go beyond
> Proof General at all.

I do, otherwise I wouldn't be using jedit in teaching and have also started to
use it for my research.

> I hope to get more constructive
> feedback on Isabelle/jEdit in the future, and find time to work on the small and
> big things that still need to be done.

I'm not sure what kind of contructive criticism I am supposed to give if
something does not work. My email was meant emphasize what Lars had already
expressed: namely that what you call "exceptional situations of incremental
parsing" can occur frequently. Lars is happy with the cut-and-repaste
workaround, but I prefer not needing a workaround.

Tobias





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