author | wenzelm |
Thu, 15 Mar 2012 19:48:19 +0100 | |
changeset 46948 | aae5566d6756 |
parent 43794 | 49cbbe2768a8 |
child 46961 | 5c6955f487e5 |
permissions | -rw-r--r-- |
27340 | 1 |
(* Title: Pure/ML/ml_antiquote.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Common ML antiquotations. |
|
5 |
*) |
|
6 |
||
7 |
signature ML_ANTIQUOTE = |
|
8 |
sig |
|
9 |
val variant: string -> Proof.context -> string * Proof.context |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
10 |
val macro: binding -> Proof.context context_parser -> theory -> theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
11 |
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
|
12 |
val declaration: string -> 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 |
||
16 |
structure ML_Antiquote: ML_ANTIQUOTE = |
|
17 |
struct |
|
18 |
||
19 |
(** generic tools **) |
|
20 |
||
21 |
(* ML names *) |
|
22 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36950
diff
changeset
|
23 |
structure Names = Proof_Data |
27340 | 24 |
( |
25 |
type T = Name.context; |
|
26 |
fun init _ = ML_Syntax.reserved; |
|
27 |
); |
|
28 |
||
29 |
fun variant a ctxt = |
|
30 |
let |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36950
diff
changeset
|
31 |
val names = Names.get ctxt; |
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
42468
diff
changeset
|
32 |
val (b, names') = Name.variant a names; |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36950
diff
changeset
|
33 |
val ctxt' = Names.put names' ctxt; |
27340 | 34 |
in (b, ctxt') end; |
35 |
||
36 |
||
37 |
(* specific antiquotations *) |
|
38 |
||
27379 | 39 |
fun macro name scan = ML_Context.add_antiq name |
27868 | 40 |
(fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed |
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33519
diff
changeset
|
41 |
(Context.Proof ctxt, fn background => (K ("", ""), background))))); |
27379 | 42 |
|
27340 | 43 |
fun inline name scan = ML_Context.add_antiq name |
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33519
diff
changeset
|
44 |
(fn _ => scan >> (fn s => fn background => (K ("", s), background))); |
27340 | 45 |
|
46 |
fun declaration kind name scan = ML_Context.add_antiq name |
|
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33519
diff
changeset
|
47 |
(fn _ => scan >> (fn s => fn background => |
27340 | 48 |
let |
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
49 |
val (a, background') = |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
50 |
variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) background; |
27340 | 51 |
val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n"; |
41486
82c1e348bc18
reverted 08240feb69c7 -- breaks positions of reports;
wenzelm
parents:
41376
diff
changeset
|
52 |
val body = "Isabelle." ^ a; |
27340 | 53 |
in (K (env, body), background') end)); |
54 |
||
55 |
val value = declaration "val"; |
|
56 |
||
57 |
||
58 |
||
30231 | 59 |
(** misc antiquotations **) |
27340 | 60 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
61 |
val _ = Context.>> (Context.map_theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
62 |
|
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
63 |
(inline (Binding.name "assert") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
64 |
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> |
40110 | 65 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
66 |
inline (Binding.name "make_string") (Scan.succeed ml_make_string) #> |
36162
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
35670
diff
changeset
|
67 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
68 |
value (Binding.name "binding") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
69 |
(Scan.lift (Parse.position Args.name) |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
70 |
>> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))) #> |
27340 | 71 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
72 |
value (Binding.name "theory") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
73 |
(Scan.lift Args.name >> (fn name => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
74 |
"Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name) |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
75 |
|| Scan.succeed "ML_Context.the_global_context ()") #> |
27340 | 76 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
77 |
value (Binding.name "context") (Scan.succeed "ML_Context.the_local_context ()") #> |
27340 | 78 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
79 |
inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
80 |
inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
81 |
inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> |
27340 | 82 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
83 |
macro (Binding.name "let") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
84 |
(Args.context -- |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
85 |
Scan.lift |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
86 |
(Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source))) |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
87 |
>> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))) #> |
27379 | 88 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
89 |
macro (Binding.name "note") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
90 |
(Args.context :|-- (fn ctxt => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
91 |
Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
92 |
>> (fn ((a, srcs), ths) => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
93 |
((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])]))) |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
94 |
>> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #> |
27379 | 95 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
96 |
value (Binding.name "ctyp") (Args.typ >> (fn T => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
97 |
"Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> |
27340 | 98 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
99 |
value (Binding.name "cterm") (Args.term >> (fn t => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
100 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
27340 | 101 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
102 |
value (Binding.name "cprop") (Args.prop >> (fn t => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
103 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
27340 | 104 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
105 |
value (Binding.name "cpat") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
106 |
(Args.context -- |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
107 |
Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
108 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
109 |
ML_Syntax.atomic (ML_Syntax.print_term t))))); |
27340 | 110 |
|
111 |
||
35396 | 112 |
(* type classes *) |
113 |
||
35670 | 114 |
fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => |
42360 | 115 |
Proof_Context.read_class ctxt s |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
41486
diff
changeset
|
116 |
|> syn ? Lexicon.mark_class |
35396 | 117 |
|> ML_Syntax.print_string); |
118 |
||
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
119 |
val _ = Context.>> (Context.map_theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
120 |
(inline (Binding.name "class") (class false) #> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
121 |
inline (Binding.name "class_syntax") (class true) #> |
35396 | 122 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
123 |
inline (Binding.name "sort") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
124 |
(Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
125 |
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))))); |
35396 | 126 |
|
127 |
||
35361
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
128 |
(* type constructors *) |
27340 | 129 |
|
36950 | 130 |
fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source) |
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
131 |
>> (fn (ctxt, (s, pos)) => |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
132 |
let |
42360 | 133 |
val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s; |
42468 | 134 |
val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); |
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
135 |
val res = |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
136 |
(case try check (c, decl) of |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
137 |
SOME res => res |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
138 |
| NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos)); |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
139 |
in ML_Syntax.print_string res end); |
27340 | 140 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
141 |
val _ = Context.>> (Context.map_theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
142 |
(inline (Binding.name "type_name") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
143 |
(type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
144 |
inline (Binding.name "type_abbrev") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
145 |
(type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
146 |
inline (Binding.name "nonterminal") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
147 |
(type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
148 |
inline (Binding.name "type_syntax") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
149 |
(type_name "type" (fn (c, _) => Lexicon.mark_type c)))); |
35361
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
150 |
|
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
151 |
|
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
152 |
(* constants *) |
27340 | 153 |
|
36950 | 154 |
fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source) |
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
155 |
>> (fn (ctxt, (s, pos)) => |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
156 |
let |
42360 | 157 |
val Const (c, _) = Proof_Context.read_const_proper ctxt false s; |
158 |
val res = check (Proof_Context.consts_of ctxt, c) |
|
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
159 |
handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos); |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
160 |
in ML_Syntax.print_string res end); |
27340 | 161 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
162 |
val _ = Context.>> (Context.map_theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
163 |
(inline (Binding.name "const_name") |
43794
49cbbe2768a8
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
wenzelm
parents:
43560
diff
changeset
|
164 |
(const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> |
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
165 |
inline (Binding.name "const_abbrev") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
166 |
(const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
167 |
inline (Binding.name "const_syntax") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
168 |
(const_name (fn (_, c) => Lexicon.mark_const c)) #> |
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
169 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
170 |
inline (Binding.name "syntax_const") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
171 |
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
172 |
if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
173 |
then ML_Syntax.print_string c |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
174 |
else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos))) #> |
27340 | 175 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
176 |
inline (Binding.name "const") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
177 |
(Args.context -- Scan.lift Args.name_source -- Scan.optional |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
178 |
(Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
179 |
>> (fn ((ctxt, raw_c), Ts) => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
180 |
let |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
181 |
val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
182 |
val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts)); |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
183 |
in ML_Syntax.atomic (ML_Syntax.print_term const) end)))); |
27340 | 184 |
|
46948 | 185 |
|
186 |
(* outer syntax *) |
|
187 |
||
188 |
val _ = Context.>> (Context.map_theory |
|
189 |
(value (Binding.name "keyword") |
|
190 |
(Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) => |
|
191 |
(if is_none (Thy_Header.the_keyword thy name) then |
|
192 |
ML_Syntax.atomic ("Parse.$$$ " ^ ML_Syntax.print_string name) |
|
193 |
else error ("Unknown minor keyword " ^ quote name)) |
|
194 |
handle ERROR msg => error (msg ^ Position.str_of pos))))); |
|
195 |
||
27340 | 196 |
end; |
197 |