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