[isabelle-dev] isabelle-dev and ML files

[Makarius]

On Fri, 23 Oct 2009, Timothy Bourke wrote:

> I'm having some trouble working with ML files in recent dev versions.
>
> Given, for example, a file test.ML:
>  structure Test =
>  struct
>    val s1 = "\<top>";
>    val s2 = "\\<top>";
>  end;
>
> And two tests:
>  ML) Direct ML: isabelle-process < test.ML
> USE) Interactive isabelle: use "test.ML";
>
> I get the following results for Isabelle 2009 and a recent (yesterday)
> dev version:
>      \            version
>  test \     2009          dev
>        +-------------+------------+
>    ML  |  s1 fails   |  s1 fails  |
>        |  s2 works   |  s2 works  |
>        +-------------+------------+
>    USE |  s1 works   |  s1 works  |
>        |  s2 works   |  s2 fails  |
>        +-------------+------------+
>
> Is the dev behaviour correct?

Shouldn't the status of s1 and s2 be swapped in ML/dev?

Which version are you using anyway?  In the face of non-linear distributed 
history with time-jumps, only the offical changeset id counts, e.g. 
fe29679cabc2 in my case ("hg id" helps to figure this out).

The 'ML' and 'use' commands operate exactly the same way, and invoking the 
"use" function from the raw ML toplevel should coincide with that. All of 
this treats Isabelle symbols as native content of the ML sources, so there 
is no longer that extra escaping (this oddity was occasionally causing 
confusion in the past, and had to dissappear altogether when precise 
counting of source positions was introduced.)

This means that ML sources with Isabelle symbols cannot be pasted into the 
raw ML loop.  In practive you need a proper context anyway (for 
antiquotations etc.) so it is best to work trough Isar/ML all the time, 
unless you do really low-level work on the ML system itself.


 	Makarius