Email Gateway (Jan 06 2021 at 14:43): 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
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
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
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: Jan 04 2025 at 20:18 UTC