[isabelle-dev] Naming context of ROOT.ML and similar.

[Makarius]

On Fri, 12 Feb 2010, Florian Haftmann wrote:

> I personally recommend to use ROOT.ML files only for a single use_thy 
> which points to the root theory of a session -- they are an artifact 
> from times when ML was the control environment, not Isar;

To illustrate this further compare these two versions of HOL/ROOT.ML:

http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009-1/src/HOL/ROOT.ML
http://isabelle.in.tum.de/repos/isabelle/file/ff1574a81019/src/HOL/ROOT.ML

In ancient times, the raw ML toplevel was used to "assemble" a certain
global environment.  Later the theory loader and Isar toplevel started 
managing more and more of this implicitly.  The present value-oriented ML 
environment within the theory context as two main benefits:

   * direct value-oriented undo of ML bindings (*no* undo of side-effects
     on reference variables, though)

   * independent (parallel) invocations of the ML compiler


> ROOT.ML files with "features" make it difficult if not impossible to use 
> a session interactively using PG.

Indeed.  In the coming convergence of interactive vs. batch "sessions", 
this will become even more relevant.  Root files with "ML scripts" will 
become awkward and slow, because Isar can do less implicit management.


 	Makarius