[isabelle] Isabelle2016-RC2 -- Misleading error message if bad theory name in addition to error in theory
I discovered an error reporting behavior of isabelle that might be misleading.
Assume I have a file bar.thy.
The file contains
In the output field, I get the expected error message:
Bad theory name "foo" for file "bar.thy"
However, if I change the file to the following, the error reporting
Now jEdit presents a red exclamation mark right next to "baz" and the error is:
Outer syntax errorâ: command expected,
but identifier bazâ was found
The error about the bad theory name is no longer reported.
Expected behavior: The first error is the wrong theory name and should
be reported first.
Circumstances how I triggered this:
I triggered this behavior when I copy-pasted a theory. The theory had
many other theories imported. One of them defined the command "baz".
Because of the bad theory name, jEdit did not load the theory which
defined "baz". But jEdit displayed an error at baz. It took a few
minutes of debugging the call to baz to figure out that the error was
This archive was generated by a fusion of
Pipermail (Mailman edition) and