author | wenzelm |
Fri, 16 Apr 2021 23:16:00 +0200 | |
changeset 73586 | 76d0b6597c91 |
parent 73551 | 53c148e39819 |
child 74291 | b83fa8f3a271 |
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 |
73549
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
9 |
val value_decl: string -> string -> Proof.context -> |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
10 |
(Proof.context -> string * string) * Proof.context |
56205 | 11 |
val declaration: binding -> 'a context_parser -> |
73549
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
12 |
(Token.src -> 'a -> Proof.context -> (Proof.context -> string * string) * Proof.context) -> |
56205 | 13 |
theory -> theory |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
14 |
val declaration_embedded: binding -> 'a context_parser -> |
73549
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
15 |
(Token.src -> 'a -> Proof.context -> (Proof.context -> string * string) * Proof.context) -> |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
16 |
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 inline: binding -> string context_parser -> theory -> theory |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
18 |
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
|
19 |
val value: binding -> string context_parser -> theory -> theory |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
20 |
val value_embedded: binding -> string context_parser -> theory -> theory |
73550
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
21 |
val special_form: binding -> string -> theory -> theory |
73586 | 22 |
val conditional: binding -> (Proof.context -> bool) -> theory -> theory |
27340 | 23 |
end; |
24 |
||
56072 | 25 |
structure ML_Antiquotation: ML_ANTIQUOTATION = |
27340 | 26 |
struct |
27 |
||
56205 | 28 |
(* define antiquotations *) |
29 |
||
73549
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
30 |
fun value_decl a s ctxt = |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
31 |
let |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
32 |
val (b, ctxt') = ML_Context.variant a ctxt; |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
33 |
val env = "val " ^ b ^ " = " ^ s ^ ";\n"; |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
34 |
val body = ML_Context.struct_name ctxt ^ "." ^ b; |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
35 |
fun decl (_: Proof.context) = (env, body); |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
36 |
in (decl, ctxt') end; |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
37 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
38 |
local |
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 |
fun gen_declaration name embedded scan body = |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
41 |
ML_Context.add_antiquotation name embedded |
73549
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
42 |
(fn range => fn src => fn orig_ctxt => |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
43 |
let |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
44 |
val (x, _) = Token.syntax scan src orig_ctxt; |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
45 |
val (decl, ctxt') = body src x orig_ctxt; |
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
46 |
in (decl #> apply2 (ML_Lex.tokenize_range range), ctxt') end); |
27340 | 47 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
48 |
fun gen_inline name embedded scan = |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
49 |
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
|
50 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
51 |
fun gen_value name embedded scan = |
73549
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
52 |
gen_declaration name embedded scan (fn _ => value_decl (Binding.name_of name)); |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
53 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
54 |
in |
27340 | 55 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
56 |
fun declaration name = gen_declaration name false; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
57 |
fun declaration_embedded name = gen_declaration name true; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
58 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
59 |
fun inline name = gen_inline name false; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
60 |
fun inline_embedded name = gen_inline name true; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
61 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
62 |
fun value name = gen_value name false; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
63 |
fun value_embedded name = gen_value name true; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
64 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
65 |
end; |
27340 | 66 |
|
67 |
||
73586 | 68 |
(* ML macros *) |
73550
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
69 |
|
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
70 |
fun special_form binding operator = |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
71 |
ML_Context.add_antiquotation binding true |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
72 |
(fn _ => fn src => fn ctxt => |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
73 |
let |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
74 |
val (s, _) = Token.syntax (Scan.lift Args.embedded_input) src ctxt; |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
75 |
val tokenize = ML_Lex.tokenize_range Position.no_range; |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
76 |
val tokenize_range = ML_Lex.tokenize_range (Input.range_of s); |
73551 | 77 |
|
78 |
val (decl, ctxt') = ML_Context.expand_antiquotes (ML_Lex.read_source s) ctxt; |
|
79 |
fun decl' ctxt'' = |
|
73550
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
80 |
let |
73551 | 81 |
val (ml_env, ml_body) = decl ctxt''; |
82 |
val ml_body' = |
|
83 |
tokenize "let val expr = (fn () => " @ ml_body @ tokenize ");" @ |
|
73550
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
84 |
tokenize " val " @ tokenize_range "result" @ |
73551 | 85 |
tokenize (" = " ^ operator ^ " expr; in result end"); |
86 |
in (ml_env, ml_body') end; |
|
87 |
in (decl', ctxt') end); |
|
73550
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
88 |
|
73586 | 89 |
fun conditional binding check = |
90 |
ML_Context.add_antiquotation binding true |
|
91 |
(fn _ => fn src => fn ctxt => |
|
92 |
let val (s, _) = Token.syntax (Scan.lift Args.embedded_input) src ctxt in |
|
93 |
if check ctxt then |
|
94 |
ML_Context.expand_antiquotes (ML_Lex.read_source s) ctxt |
|
95 |
else (K ([], []), ctxt) |
|
96 |
end); |
|
97 |
||
73550
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73549
diff
changeset
|
98 |
|
56205 | 99 |
(* basic antiquotations *) |
27340 | 100 |
|
53171 | 101 |
val _ = Theory.setup |
64556 | 102 |
(declaration (Binding.make ("here", \<^here>)) (Scan.succeed ()) |
59112 | 103 |
(fn src => fn () => |
73549
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
69592
diff
changeset
|
104 |
value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #> |
56071 | 105 |
|
64556 | 106 |
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
|
107 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
108 |
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
|
109 |
(Scan.lift (Parse.input Args.embedded) >> (ML_Syntax.make_binding o Input.source_content)) #> |
62850 | 110 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
111 |
value_embedded (Binding.make ("cartouche", \<^here>)) |
62850 | 112 |
(Scan.lift Args.cartouche_input >> (fn source => |
113 |
"Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^ |
|
69470 | 114 |
ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #> |
115 |
||
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69470
diff
changeset
|
116 |
inline_embedded (Binding.make ("verbatim", \<^here>)) |
69470 | 117 |
(Scan.lift Args.embedded >> ML_Syntax.print_string)); |
46948 | 118 |
|
27340 | 119 |
end; |