[isabelle-dev] isabelle-dev and ML files

[Timothy Bourke]

On Oct 23 at 16:32 +0200, Makarius wrote:
> 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?

I'm reasonably sure that the table is accurate.
 
> 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).

b8ca12f6681a
 
> 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.)

I agree that, within an isabelle session, 'ML' and 'use' are
consistent.
 
> 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.

Ok. This was my point.

It used to be possible to test modifications to isabelle source files
containing \<...> symbols, from within emacs, by typing:
    ML {* use "src/Pure/Thy/html.ML" *}

But I can understand that this change is only likely to affect a few
people, and, even then, not very often.

Thank you for the explanations.

Tim.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 187 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091026/556be84a/attachment.sig>