Re: [isabelle] Isabelle/jEdit: Multiline Comments/Reparsing

On Sun, 27 May 2012, Steffen J. Smolka wrote:

when working with jEdit, Isabelle sometimes gets stuck and displays error messages even though the input is actually valid. For example, this happens when I try to comment out a block containing a blank line. It also happens occasionally when simply defining a function or formulating a lemma or theorem.

Is there a better way to reparse a file (or part of a file) than closing and reopening the file? This can be a real pain, especially with large theories.

This feature is documented in the README that you get when starting Isabelle/jEdit for the first time (and until you undock that window). See the section "Limitations and workarounds (May 2012)", and possibly also "Known problems with Mac OS X (Java 1.6)".


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