Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC