author | wenzelm |
Wed, 19 Aug 2015 16:21:10 +0200 | |
changeset 60975 | 5f3d6e16ea78 |
parent 59112 | e670969f34df |
child 62662 | 291cc01f56f5 |
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 |
56205 | 9 |
val declaration: binding -> 'a context_parser -> |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57832
diff
changeset
|
10 |
(Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) -> |
56205 | 11 |
theory -> theory |
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
12 |
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
|
13 |
val value: binding -> string context_parser -> theory -> theory |
27340 | 14 |
end; |
15 |
||
56072 | 16 |
structure ML_Antiquotation: ML_ANTIQUOTATION = |
27340 | 17 |
struct |
18 |
||
56205 | 19 |
(* define antiquotations *) |
20 |
||
21 |
fun declaration name scan body = |
|
22 |
ML_Context.add_antiquotation name |
|
23 |
(fn src => fn orig_ctxt => |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57832
diff
changeset
|
24 |
let val (x, _) = Token.syntax scan src orig_ctxt |
56205 | 25 |
in body src x orig_ctxt end); |
27340 | 26 |
|
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53163
diff
changeset
|
27 |
fun inline name scan = |
56205 | 28 |
declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt)); |
27340 | 29 |
|
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53163
diff
changeset
|
30 |
fun value name scan = |
59112 | 31 |
declaration name scan (fn _ => ML_Context.value_decl (Binding.name_of name)); |
27340 | 32 |
|
33 |
||
56205 | 34 |
(* basic antiquotations *) |
27340 | 35 |
|
53171 | 36 |
val _ = Theory.setup |
56436 | 37 |
(declaration (Binding.make ("here", @{here})) (Scan.succeed ()) |
59112 | 38 |
(fn src => fn () => |
39 |
ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #> |
|
56071 | 40 |
|
56436 | 41 |
value (Binding.make ("binding", @{here})) |
56205 | 42 |
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding)); |
46948 | 43 |
|
27340 | 44 |
end; |
45 |