Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Error messages in RC2014-RC4


view this post on Zulip Email Gateway (Aug 19 2022 at 15:39):

From: Alfio Martini <alfio.martini@acm.org>
Dear Makarius,

Maybe it is a little too late for that, but I have just noticed that error
messages in the RC4 version are showing a strange typographical
symbol. I think there is something to be adjusted here. See image
for an example. I am using the Windows version.

The messages are fine in the current official version (2013-2).

Best!
strange_error_message.PNG

view this post on Zulip Email Gateway (Aug 19 2022 at 15:39):

From: Lars Noschinski <noschinl@in.tum.de>
This is intended: Ctrl+clicking on this symbol takes you to the position
of the error.

-- Lars

view this post on Zulip Email Gateway (Aug 19 2022 at 15:40):

From: Alfio Martini <alfio.martini@acm.org>
Thank you Lars! It does not seem to be of any use, though. The position
errors are
already marked with squiggly red underlines.

Best!

view this post on Zulip Email Gateway (Aug 19 2022 at 15:40):

From: Lars Noschinski <noschinl@in.tum.de>
It is very useful for errors in ML blocks or if those errors refer to an
exception in some ML-code.


Last updated: May 06 2024 at 16:21 UTC