[isabelle-dev] Remaining uses of Proof General?
lammich at in.tum.de
Fri Jun 27 13:58:34 CEST 2014
> That clickable area is convenient, but not strictly necessary. It is
> absent in PG anyway. Whenever the Prover IDE outputs an error message,
> e.g. in tooltips or the Output panel, it includes the source position
> information, *if* that is available.
The problem is, that I cannot make the output panel display the error
message, or get a tooltip on the error message, without *first* locating
its position in the editor window!?
Following example: Slightly change the simpset, and try to load
$AFP/Automatic_Refinement/Lib/Misc.thy, a 4400 lines beast. Change the
simpset so that it fails somewhere in the middle of the theory.
I only see a red mark in the theory-panel, but how do I navigate to the
In PG, I actually saw file-name/line-number/error-message. In
Isabelle/jEdit, the only way I know is to open the file, hope that the
text-overview column displays the error already, and try a precise
mouse-click to get to the location. If the error-column does not display
the error, because it is not within the limit, I have to scroll through
the file manually.
So am I missing some feature here that makes the workflow
"Navigate to an error in a theory file"
More information about the isabelle-dev