*To*: Lucas Dixon <ldixon at inf.ed.ac.uk>*Subject*: Re: [isabelle] antiquotations*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Thu, 14 Feb 2008 13:23:27 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Makarius <makarius at sketis.net>, Alexander Krauss <krauss at in.tum.de>*In-reply-to*: <47B381D7.7050908@inf.ed.ac.uk>*References*: <478AAC94.3030404@rsise.anu.edu.au> <478B2940.5020107@informatik.tu-muenchen.de> <478BEE3B.2000007@rsise.anu.edu.au> <478C8265.2010202@in.tum.de> <478D322C.7010001@rsise.anu.edu.au> <478DB7F0.7080604@in.tum.de> <478E6F17.9000100@rsise.anu.edu.au> <478E816D.9010606@in.tum.de> <478EF53A.9070809@rsise.anu.edu.au> <Pine.LNX.4.63.0801241542360.18967@atbroy100.informatik.tu-muenchen.de> <47ABC81B.3090608@rsise.anu.edu.au> <Pine.LNX.4.63.0802081405450.9643@atbroy100.informatik.tu-muenchen.de> <47AF877C.4050205@rsise.anu.edu.au> <47B04E56.7010901@in.tum.de> <47B381D7.7050908@inf.ed.ac.uk>*User-agent*: Icedove 1.5.0.14pre (X11/20071018)

Lucas Dixon wrote:

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Alexander Krauss wrote:Since bind_thms is impure, it can only update some global reference hanging around. This is incompatible with paralellism. At the moment it may work sometimes, but it is guaranteed to break sooner or later.I'm curious about this: is it really the case that references are inherently incompatible with parallelism? Is there some reason why it cannot update a thread-local reference? I would expect that you can cut the Isar/ML cake both ways: anti-quotations in Isar or quotations in ML. I feel there should be a confluence proof there somewhere :) So, is there some reason this is not possible? In particular, Isar is executed in ML, so it seems rather strange to me that you cannot replicate it's effect in ML, for example by pasting the function calls used by Isar into the ML. cheers, lucas

Lucas / Alexander, Well, yes, one would think so. Perusing the source code, I see a function called eval_antiquotes (to be exact, I used !ML_Context.eval_antiquotes_fn) which gives results like this: val eval_antiquotes = !ML_Context.eval_antiquotes_fn ; eval_antiquotes "val x = y ; val c = @{context} ; \ \ val a = b ; val cs = @{claset} ; val t = @{theory}" ; val eval_antiquotes = fn : string -> string * string > # val it =

: string * string Is this in fact used when the system encounters code such as ML {* val x = y ; val c = @{context} ; \ \ val a = b ; val cs = @{claset} ; val t = @{theory} *} ?

ML {* ... *} ? If not, what exactly does happen ?

In terms of threads in general:

Regards, Jeremy

**Follow-Ups**:**Re: [isabelle] antiquotations***From:*Makarius

**References**:**Re: [isabelle] antiquotations***From:*Jeremy Dawson

**Re: [isabelle] antiquotations***From:*Makarius

**Re: [isabelle] antiquotations***From:*Jeremy Dawson

**Re: [isabelle] antiquotations***From:*Alexander Krauss

**Re: [isabelle] antiquotations***From:*Lucas Dixon

- Previous by Date: Re: [isabelle] antiquotations
- Next by Date: Re: [isabelle] interpretations and polymorphism
- Previous by Thread: Re: [isabelle] antiquotations
- Next by Thread: Re: [isabelle] antiquotations
- Cl-isabelle-users February 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list