[isabelle-dev] jEdit Output Panel

Christian Sternagel c-sterna at jaist.ac.jp
Mon Aug 27 07:25:37 CEST 2012


Dear Makarius,

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.

cheers

chris


More information about the isabelle-dev mailing list