[isabelle-dev] Remaining uses of Proof General?

[Peter Lammich]

> 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
error location?

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"
simpler?


--
  Peter