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

[Florian Haftmann]

Hi Thomas,

> It would appear that with Isabelle-2009-1, the ROOT.ML or similar ML
> file called by isabelle usedir isn't allowed to do anything. Or at
> least, it's not allowed to know about any useful structures.

ML plays two roles for Isabelle:

* it is the language the framework Pure is implemented in
* it is the language which allows to extend the system on top of the
Isar infrastructure.

Taking the second aspect seriously, all definitions done in ML after the
bootstrap of Pure are under the control of Isar; in particular, in
nearly all of the cases they happen within a certain theory, which in
consequence means that each theory has its own ML context part which is
administrated like any other theory data (constants, definitions, types,
records, whatever ...) with proper merges on theory import etc.
Therefore, outside any theory, there are just the bare bones of the
framework available at the toplevel.  Referring to "the" ML context
makes no sense here.

So, in your case you should put your ML code into an ML {* *} or
ML_command {* *} block within a theory.

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;  ROOT.ML files
with "features" make it difficult if not impossible to use a session
interactively using PG.


Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 260 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100212/b165d514/attachment.sig>