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