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
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