Email Gateway (Aug 18 2022 at 19:57): Email Gateway (Aug 18 2022 at 19:57):From: "Steffen J. Smolka" <steffen.smolka@in.tum.de>
Hi all,
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.
Best Regards
Steffen
Email Gateway (Aug 18 2022 at 19:57):From: Lars Noschinski <noschinl@in.tum.de>
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
Email Gateway (Aug 18 2022 at 19:58):From: Makarius <makarius@sketis.net>
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)".
Makarius
Last updated: Nov 21 2024 at 12:39 UTC