Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] marginal comments in Isabelle2018-RC3


view this post on Zulip 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: Mar 28 2024 at 20:16 UTC