[isabelle] Isabelle2016-RC2 -- Misleading error message if bad theory name in addition to error in theory



Hi,

I discovered an error reporting behavior of isabelle that might be misleading.

Assume I have a file bar.thy.

The file contains
theory foo
imports
  Main
begin

end

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
gets misleading:

theory foo
imports
  Main
begin
  baz
end

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
somewhere else.


Best Regards
  Cornelius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.