Re: [isabelle] Isabelle2015-RC0 available for testing

On Sun, 12 Apr 2015, C. Diekmann wrote:

I found a "feature request" for the jEdit interface: I loaded WordLemmaBucket from autocorres, a file with 5900 lines. There are at least two errors near the end of the file when loading with 2015-RC0. However, it is nearly impossible to locate the errors in the .thy.

Where can I see this file?

Is it possible to have some sort of "jump to next error" or an automatic jump to the error when I click on the red spot (left of the jEdit scroll bar)?

This feature is still not there after several years, because other things had a much higher priority.

Also, when I have an error in my theory, e.g. writing "where f=..." but in 2015-RC0 it should be "where f1=...", only the "f" is underlined, this makes the error quite hard to spot for me.

That is a consequence of a more precise error position: it is a normal trend in ongoing PIDE conformity improvements.

What is your font size? (Mine is 30px on a 4K display.) The error should be also visible in the Output panel.


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