Isabelle/94b2690ad494 is a notable point in history where outer syntax
follows the theory structure just like anything else: the odd implicit
global state has been removed, both in ML and Scala. This also means that
"keywords" in the theory header affect Isabelle/jEdit syntax highlighting
and completion etc. of the underlying editor buffer.
This reform has required countless years, but after the recent deletion of
the TTY loop it became feasible. If anything has been forgotten or causes
surprises, please report observations here.
Makarius
----------------------------------------------------------------------------
http://stop-ttip.org 999,921 people so far
----------------------------------------------------------------------------
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
