[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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