Re: [isabelle] Isabelle2015-RC0 available for testing



On Mon, 13 Apr 2015, C. Diekmann wrote:

I found an inconvenient jEdit error reporting behavior:

I loaded theory A

theory A imports B C D E

Isabelle does not load my theory A and stops processing. I get the
same behavior as if there is an error somewhere in the imported files
B C D E. However, jEdit does not show me an error message. Let's say
theory C starts the following:

theory C imports "$VAR/XYZ"

where $VAR is an environment variable usually set in my Linux
environment, which I accidentally misspelled. When I open theory C, I
get the expected error message "Undefined environment variable: VAR".
However, it is hard to find that the error is in theory C because the
theory panel does not display an error and in theory A, there is also
no indication why isabelle does not process it.

This should work in Isabelle2015-RC2.


	Makarius





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