Email Gateway (Aug 22 2022 at 17:44): Email Gateway (Aug 22 2022 at 17:44):From: Dominique Unruh <unruh@ut.ee>
While this doesn't fix the problem, it may be useful to know:
If you use the goto-error.bsh script (that was sent on this mailing list
recently), it will find the error.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 17:44):From: Makarius <makarius@sketis.net>
On 30/07/18 20:13, Fabian Hellauer wrote:
theory Scratch imports
Main
begin― ‹dummy mistake: @{term ‹if True then Suc else 0›}›
end
In Isabelle2018-RC3, I see no way to read the error message from within
Isabelle/jEdit:
The Theories panel indicates an error, but not the main text area or the
bars next to it.
There is a delicate problem behind it, concerning the range of the
command space: trailing formal comments need to be included, while
informal ones are excluded since Isabelle/88c6e630c15f (24-Sep-2018).
I have now refined for the next release candidate:
https://isabelle.sketis.net/repos/isabelle-release/rev/3a02b424d5fb
PS: The reference manual mentions two forms of marginal comments in
section 3.3.5:
One with \<comment> and one with "—". Aren't these the same?
They are the same after decoding of symbols in the PIDE front-end, e.g.
Isabelle/jEdit. The manual is a bit vague about such details: sometimes
it talks about verbatim symbols like \<comment> sometimes the rendered
versions, sometimes both within the same sentence as above.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC