Email Gateway (Aug 22 2022 at 17:44): Email Gateway (Aug 22 2022 at 17:44):From: Fabian Hellauer <hellauer@in.tum.de>
Makarius,
consider the following theory with an erroneous antiquotation:
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.
Fabian
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?
Last updated: Nov 21 2024 at 12:39 UTC