On Fri, 27 Jun 2014, Peter Lammich wrote:
* Isabelle/jEdit does not scale to large files. Error markers on the
right side are only displayed for a context around the current cursor
position. There seems to be no way to jump to the error position. If the
error happens to be displayed as a red bar on the right side of the
editor area, pixel-accurate mousing is required to jump to the error,
and not to a position dozens of lines away.
This needs more specific information about the experimental setup. What
means "large"? Where were the errors coming from?
The so-called "text overview" column is indeed a performance bottle-neck.
It is restricted by default to a portion of the text buffer, to avoid
problems with real-time rendering of exessivley large files. See also the
system option jedit_text_overview_limit -- its default value 65536 is some
kind of insider-joke. You can try to enlarge that a bit, depending on
your hardware performance.
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. In the repository versions we are
talking about here, there is a \<here> symbol that is rendered as a
Unicode "house" (for "home position"). It replaces the textual
representation from the past TTY era: "(line 42 of file foo)". That
symbol can be used as hyperlink using the normal PIDE idioms.
If the latter is missing, their might be a problem with the tool that
emitted the error message.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
