> 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev