Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2021-RC1 - error highlighting


view this post on Zulip Email Gateway (Jan 06 2021 at 14:43):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,

The error highlighting does not include the tactics anymore:

Is that the expected behavior? I find error harder to find in a buffer.

Best,

Mathias
lepejeaojnilcbgn.png

view this post on Zulip Email Gateway (Jan 07 2021 at 13:58):

From: Makarius <makarius@sketis.net>
So what is actually the error? (It would be better to have a reproducible
example).

Here is an example that works:

theory Scratch
imports FOL
begin

lemma A B C by auto

end

As expected, the error for the proof method (not tactic) "auto" is "Failed to
apply initial proof method" over the text "auto".

Makarius

view this post on Zulip Email Gateway (Jan 07 2021 at 15:40):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hello Makarius,

The error is that the red error highlighting (the big red background
that is shown in Isabelle/jEdit) does not extend past the "by". Here a
screenshot with Isabelle 2020 and 2021-RC1 for comparison:

I prefer the old behavior, but the new one is consistent. This happens
on every error wrong "by", which is why I did not provide a theory. The
one from the screenshot is:

theory Scratch
  imports Main
begin
lemma A B C by auto
end

Mathias
ffianododginnbng.png

view this post on Zulip Email Gateway (Jan 08 2021 at 20:18):

From: Makarius <makarius@sketis.net>
On 07/01/2021 16:40, Mathias Fleury wrote:

The error is that the red error highlighting (the big red background that is
shown in Isabelle/jEdit) does not extend past the "by". Here a screenshot with
Isabelle 2020 and 2021-RC1 for comparison:

I prefer the old behavior, but the new one is consistent. This happens on
every error wrong "by", which is why I did not provide a theory.

I have studied the history in more detail. The old behaviour was a consequence of

changeset: 49037:d7a1973b063c
user: wenzelm


Last updated: Dec 05 2021 at 22:18 UTC