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



On 27.05.2012 21:30, 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.

The best workaround at this time is to cut and paste the wrongly parsed block. If you comment something out, this means cutting and pasting the whole comment.

  -- Lars





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