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

On Tue, 22 May 2012, Tobias Nipkow wrote:

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.

I also prefer not requiring such workarounds, but for me this feature only occurrs in exceptional situations. This is why it got a lower priority in the list of things to work on.

Since the balancing problem of quotes/comments is a common problem of IDEs, maybe someone on the mailing list can point to solutions that other people have found for it. For example, Netbeans makes it hard to type unbalanced quotes/comments at all by closing the range immediately, but I did not like the mechanics of it very much.


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