author | wenzelm |
Thu, 07 Apr 2016 13:35:08 +0200 | |
changeset 62899 | 845ed4584e21 |
parent 62850 | 1f1a2c33ccf4 |
child 62900 | c641bf9402fd |
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 |
|
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
59112
diff
changeset
|
41 |
inline (Binding.make ("make_string", @{here})) |
62899
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62850
diff
changeset
|
42 |
(Args.context >> (ML_Pretty.make_string_local o ML_Context.struct_name)) #> |
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
59112
diff
changeset
|
43 |
|
56436 | 44 |
value (Binding.make ("binding", @{here})) |
62850 | 45 |
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #> |
46 |
||
47 |
value (Binding.make ("cartouche", @{here})) |
|
48 |
(Scan.lift Args.cartouche_input >> (fn source => |
|
49 |
"Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^ |
|
50 |
ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source))))); |
|
46948 | 51 |
|
27340 | 52 |
end; |