[isabelle-dev] jEdit Output Panel

[Makarius]

On Mon, 27 Aug 2012, Christian Sternagel wrote:

> I just started to play around with the latest and greatest 
> Isabelle/jEdit (there have been several promising commits during my 
> absence).
>
> Now I wanted to file a bagatelle ;). (I'm on changeset 10b89c127153.) Minimal 
> example:
> - start Isabelle/jEdit
> - type "theory Scratch" (observe the output panel while typing)
> we get: "Outer syntax error: keyword "begin" expected, but end-of-file was 
> found"
> - continue typing "imports Main begin"
> we still have "Outer syntax error: keyword "begin" expected, but end-of-file 
> was found" in the output panel (although no errors are indicated in the main 
> buffer or the gutter anymore).
>
> It seems as if the output panel is slightly "out-of-sync" w.r.t. the cursor.

See now Isabelle/c1ca931b3647, which hopefully makes the behaviour more 
expected.

The problem behind it is that jEdit treats the very end of buffer 
specially, with one less character than expected, such that the caret 
points nowhere instead of the end-of-text.

I've filed a tracker item of this observation many month ago to the jEdit 
source-forge project, but lost track of what happened with it.


 	Makarius