Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2016-1-RC0: error markup too large

Email Gateway (Aug 22 2022 at 14:15):

From: Lars Hupel <hupel@in.tum.de>
Dear Makarius,

it seems that in some situations, the "error" markup covers a too large
region. Here's a small example:

lemma True
proof -
have False
sorry

―‹abc›

The comment is also highlighted in red.

Cheers
Lars

Last updated: Apr 24 2024 at 08:20 UTC