[isabelle-dev] Outer syntax based on theory structure

[Makarius]

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
----------------------------------------------------------------------------