author | haftmann |
Thu, 01 May 2014 09:30:35 +0200 | |
changeset 56811 | b66639331db5 |
parent 56436 | 30ccec1e82fb |
child 57832 | 5b48f2047c24 |
permissions | -rw-r--r-- |
56072 | 1 |
(* Title: Pure/ML/ml_antiquotation.ML |
27340 | 2 |
Author: Makarius |
3 |
||
56205 | 4 |
ML antiquotations. |
27340 | 5 |
*) |
6 |
||
56072 | 7 |
signature ML_ANTIQUOTATION = |
27340 | 8 |
sig |
9 |
val variant: string -> Proof.context -> string * Proof.context |
|
56205 | 10 |
val declaration: binding -> 'a context_parser -> |
11 |
(Args.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) -> |
|
12 |
theory -> theory |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
13 |
val inline: binding -> string context_parser -> theory -> theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
14 |
val value: binding -> string context_parser -> theory -> theory |
27340 | 15 |
end; |
16 |
||
56072 | 17 |
structure ML_Antiquotation: ML_ANTIQUOTATION = |
27340 | 18 |
struct |
19 |
||
56205 | 20 |
(* unique names *) |
27340 | 21 |
|
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
48646
diff
changeset
|
22 |
val init_context = ML_Syntax.reserved |> Name.declare "ML_context"; |
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
48646
diff
changeset
|
23 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36950
diff
changeset
|
24 |
structure Names = Proof_Data |
27340 | 25 |
( |
26 |
type T = Name.context; |
|
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
48646
diff
changeset
|
27 |
fun init _ = init_context; |
27340 | 28 |
); |
29 |
||
30 |
fun variant a ctxt = |
|
31 |
let |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36950
diff
changeset
|
32 |
val names = Names.get ctxt; |
56811 | 33 |
val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names; |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36950
diff
changeset
|
34 |
val ctxt' = Names.put names' ctxt; |
27340 | 35 |
in (b, ctxt') end; |
36 |
||
37 |
||
56205 | 38 |
(* define antiquotations *) |
39 |
||
40 |
fun declaration name scan body = |
|
41 |
ML_Context.add_antiquotation name |
|
42 |
(fn src => fn orig_ctxt => |
|
43 |
let val (x, _) = Args.syntax scan src orig_ctxt |
|
44 |
in body src x orig_ctxt end); |
|
27340 | 45 |
|
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53163
diff
changeset
|
46 |
fun inline name scan = |
56205 | 47 |
declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt)); |
27340 | 48 |
|
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53163
diff
changeset
|
49 |
fun value name scan = |
56205 | 50 |
declaration name scan (fn _ => fn s => fn ctxt => |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
51 |
let |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
52 |
val (a, ctxt') = variant (Binding.name_of name) ctxt; |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
53 |
val env = "val " ^ a ^ " = " ^ s ^ ";\n"; |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
54 |
val body = "Isabelle." ^ a; |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
55 |
in (K (env, body), ctxt') end); |
27340 | 56 |
|
57 |
||
56205 | 58 |
(* basic antiquotations *) |
27340 | 59 |
|
53171 | 60 |
val _ = Theory.setup |
56436 | 61 |
(declaration (Binding.make ("here", @{here})) (Scan.succeed ()) |
56071 | 62 |
(fn src => fn () => fn ctxt => |
63 |
let |
|
64 |
val (a, ctxt') = variant "position" ctxt; |
|
65 |
val (_, pos) = Args.name_of_src src; |
|
66 |
val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n"; |
|
67 |
val body = "Isabelle." ^ a; |
|
68 |
in (K (env, body), ctxt') end) #> |
|
69 |
||
56436 | 70 |
value (Binding.make ("binding", @{here})) |
56205 | 71 |
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding)); |
46948 | 72 |
|
27340 | 73 |
end; |
74 |