author | nipkow |
Tue, 05 Nov 2019 14:57:41 +0100 | |
changeset 71033 | c1b63124245c |
parent 69592 | a80d8ec6c998 |
child 73549 | a2c589d5e1e4 |
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 |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
12 |
val declaration_embedded: binding -> 'a context_parser -> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
13 |
(Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) -> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
14 |
theory -> theory |
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
15 |
val inline: binding -> string context_parser -> theory -> theory |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
16 |
val inline_embedded: binding -> string context_parser -> theory -> theory |
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
17 |
val value: binding -> string context_parser -> theory -> theory |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
18 |
val value_embedded: binding -> string context_parser -> theory -> theory |
27340 | 19 |
end; |
20 |
||
56072 | 21 |
structure ML_Antiquotation: ML_ANTIQUOTATION = |
27340 | 22 |
struct |
23 |
||
56205 | 24 |
(* define antiquotations *) |
25 |
||
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
26 |
local |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
27 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
28 |
fun gen_declaration name embedded scan body = |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
29 |
ML_Context.add_antiquotation name embedded |
56205 | 30 |
(fn src => fn orig_ctxt => |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57832
diff
changeset
|
31 |
let val (x, _) = Token.syntax scan src orig_ctxt |
56205 | 32 |
in body src x orig_ctxt end); |
27340 | 33 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
34 |
fun gen_inline name embedded scan = |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
35 |
gen_declaration name embedded scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt)); |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
36 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
37 |
fun gen_value name embedded scan = |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
38 |
gen_declaration name embedded scan (fn _ => ML_Context.value_decl (Binding.name_of name)); |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
39 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
40 |
in |
27340 | 41 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
42 |
fun declaration name = gen_declaration name false; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
43 |
fun declaration_embedded name = gen_declaration name true; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
44 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
45 |
fun inline name = gen_inline name false; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
46 |
fun inline_embedded name = gen_inline name true; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
47 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
48 |
fun value name = gen_value name false; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
49 |
fun value_embedded name = gen_value name true; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
50 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
51 |
end; |
27340 | 52 |
|
53 |
||
56205 | 54 |
(* basic antiquotations *) |
27340 | 55 |
|
53171 | 56 |
val _ = Theory.setup |
64556 | 57 |
(declaration (Binding.make ("here", \<^here>)) (Scan.succeed ()) |
59112 | 58 |
(fn src => fn () => |
59 |
ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #> |
|
56071 | 60 |
|
64556 | 61 |
inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #> |
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
59112
diff
changeset
|
62 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
63 |
value_embedded (Binding.make ("binding", \<^here>)) |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
67146
diff
changeset
|
64 |
(Scan.lift (Parse.input Args.embedded) >> (ML_Syntax.make_binding o Input.source_content)) #> |
62850 | 65 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
66 |
value_embedded (Binding.make ("cartouche", \<^here>)) |
62850 | 67 |
(Scan.lift Args.cartouche_input >> (fn source => |
68 |
"Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^ |
|
69470 | 69 |
ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #> |
70 |
||
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
71 |
inline_embedded (Binding.make ("verbatim", \<^here>)) |
69470 | 72 |
(Scan.lift Args.embedded >> ML_Syntax.print_string)); |
46948 | 73 |
|
27340 | 74 |
end; |