author | wenzelm |
Wed, 12 Mar 2014 22:44:55 +0100 | |
changeset 56071 | 2ffdedb0c044 |
parent 56069 | 451d5b73f8cf |
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 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
|
11 |
val value: binding -> string context_parser -> theory -> theory |
27340 | 12 |
end; |
13 |
||
14 |
structure ML_Antiquote: ML_ANTIQUOTE = |
|
15 |
struct |
|
16 |
||
17 |
(** generic tools **) |
|
18 |
||
19 |
(* ML names *) |
|
20 |
||
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
48646
diff
changeset
|
21 |
val init_context = ML_Syntax.reserved |> Name.declare "ML_context"; |
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
48646
diff
changeset
|
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; |
|
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
48646
diff
changeset
|
26 |
fun init _ = init_context; |
27340 | 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; |
53170
96f7adb55d72
more robust ML_Antiquote.variant via Name.desymbolize (which also allows symbolic names, for example);
wenzelm
parents:
53169
diff
changeset
|
32 |
val (b, names') = Name.variant (Name.desymbolize false 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 |
||
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53163
diff
changeset
|
39 |
fun inline name scan = |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
40 |
ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt)); |
27340 | 41 |
|
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53163
diff
changeset
|
42 |
fun value name scan = |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
43 |
ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
44 |
let |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
45 |
val (a, ctxt') = variant (Binding.name_of name) ctxt; |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
46 |
val env = "val " ^ a ^ " = " ^ s ^ ";\n"; |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
47 |
val body = "Isabelle." ^ a; |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56002
diff
changeset
|
48 |
in (K (env, body), ctxt') end); |
27340 | 49 |
|
50 |
||
51 |
||
30231 | 52 |
(** misc antiquotations **) |
27340 | 53 |
|
53171 | 54 |
val _ = Theory.setup |
56071 | 55 |
(ML_Context.antiquotation (Binding.name "here") (Scan.succeed ()) |
56 |
(fn src => fn () => fn ctxt => |
|
57 |
let |
|
58 |
val (a, ctxt') = variant "position" ctxt; |
|
59 |
val (_, pos) = Args.name_of_src src; |
|
60 |
val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n"; |
|
61 |
val body = "Isabelle." ^ a; |
|
62 |
in (K (env, body), ctxt') end) #> |
|
63 |
||
64 |
inline (Binding.name "assert") |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
65 |
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> |
40110 | 66 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
67 |
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
|
68 |
|
51979 | 69 |
value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) => |
70 |
(Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos); |
|
71 |
ML_Syntax.print_string name))) #> |
|
51942 | 72 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
73 |
value (Binding.name "binding") |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46948
diff
changeset
|
74 |
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #> |
27340 | 75 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
76 |
value (Binding.name "theory") |
55614
e2d71b8b0d95
prefer guarded Context_Position.report where feasible;
wenzelm
parents:
55111
diff
changeset
|
77 |
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => |
e2d71b8b0d95
prefer guarded Context_Position.report where feasible;
wenzelm
parents:
55111
diff
changeset
|
78 |
(Context_Position.report ctxt pos |
e2d71b8b0d95
prefer guarded Context_Position.report where feasible;
wenzelm
parents:
55111
diff
changeset
|
79 |
(Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name)); |
e2d71b8b0d95
prefer guarded Context_Position.report where feasible;
wenzelm
parents:
55111
diff
changeset
|
80 |
"Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)) |
48781 | 81 |
|| Scan.succeed "Proof_Context.theory_of ML_context") #> |
27340 | 82 |
|
51686 | 83 |
value (Binding.name "theory_context") |
55614
e2d71b8b0d95
prefer guarded Context_Position.report where feasible;
wenzelm
parents:
55111
diff
changeset
|
84 |
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => |
e2d71b8b0d95
prefer guarded Context_Position.report where feasible;
wenzelm
parents:
55111
diff
changeset
|
85 |
(Context_Position.report ctxt pos |
e2d71b8b0d95
prefer guarded Context_Position.report where feasible;
wenzelm
parents:
55111
diff
changeset
|
86 |
(Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name)); |
e2d71b8b0d95
prefer guarded Context_Position.report where feasible;
wenzelm
parents:
55111
diff
changeset
|
87 |
"Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ |
51686 | 88 |
ML_Syntax.print_string name))) #> |
89 |
||
48781 | 90 |
inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #> |
27340 | 91 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
92 |
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
|
93 |
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
|
94 |
inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> |
27340 | 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 => |
48781 | 97 |
"Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^ |
98 |
ML_Syntax.atomic (ML_Syntax.print_typ T))) #> |
|
27340 | 99 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
100 |
value (Binding.name "cterm") (Args.term >> (fn t => |
48781 | 101 |
"Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ |
102 |
ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
|
27340 | 103 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
104 |
value (Binding.name "cprop") (Args.prop >> (fn t => |
48781 | 105 |
"Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ |
106 |
ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
|
27340 | 107 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
108 |
value (Binding.name "cpat") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
109 |
(Args.context -- |
55111 | 110 |
Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t => |
48781 | 111 |
"Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ |
53171 | 112 |
ML_Syntax.atomic (ML_Syntax.print_term t)))); |
27340 | 113 |
|
114 |
||
35396 | 115 |
(* type classes *) |
116 |
||
55111 | 117 |
fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => |
42360 | 118 |
Proof_Context.read_class ctxt s |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
41486
diff
changeset
|
119 |
|> syn ? Lexicon.mark_class |
35396 | 120 |
|> ML_Syntax.print_string); |
121 |
||
53171 | 122 |
val _ = Theory.setup |
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 "class") (class false) #> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
124 |
inline (Binding.name "class_syntax") (class true) #> |
35396 | 125 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
126 |
inline (Binding.name "sort") |
55111 | 127 |
(Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => |
53171 | 128 |
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); |
35396 | 129 |
|
130 |
||
35361
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
131 |
(* type constructors *) |
27340 | 132 |
|
55111 | 133 |
fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) |
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
134 |
>> (fn (ctxt, (s, pos)) => |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
135 |
let |
56002 | 136 |
val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s; |
42468 | 137 |
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
|
138 |
val res = |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
139 |
(case try check (c, decl) of |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
140 |
SOME res => res |
48992 | 141 |
| NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); |
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
142 |
in ML_Syntax.print_string res end); |
27340 | 143 |
|
53171 | 144 |
val _ = Theory.setup |
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
145 |
(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
|
146 |
(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
|
147 |
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
|
148 |
(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
|
149 |
inline (Binding.name "nonterminal") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
150 |
(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
|
151 |
inline (Binding.name "type_syntax") |
53171 | 152 |
(type_name "type" (fn (c, _) => Lexicon.mark_type c))); |
35361
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
153 |
|
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
154 |
|
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
155 |
(* constants *) |
27340 | 156 |
|
55111 | 157 |
fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) |
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
158 |
>> (fn (ctxt, (s, pos)) => |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
159 |
let |
56002 | 160 |
val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s; |
42360 | 161 |
val res = check (Proof_Context.consts_of ctxt, c) |
48992 | 162 |
handle TYPE (msg, _, _) => error (msg ^ Position.here pos); |
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
163 |
in ML_Syntax.print_string res end); |
27340 | 164 |
|
53171 | 165 |
val _ = Theory.setup |
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
166 |
(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
|
167 |
(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
|
168 |
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
|
169 |
(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
|
170 |
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
|
171 |
(const_name (fn (_, c) => Lexicon.mark_const c)) #> |
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
172 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
173 |
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
|
174 |
(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
|
175 |
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
|
176 |
then ML_Syntax.print_string c |
48992 | 177 |
else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #> |
27340 | 178 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
179 |
inline (Binding.name "const") |
55111 | 180 |
(Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional |
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43326
diff
changeset
|
181 |
(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
|
182 |
>> (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
|
183 |
let |
55954 | 184 |
val Const (c, _) = |
56002 | 185 |
Proof_Context.read_const {proper = true, strict = true} ctxt raw_c; |
46987 | 186 |
val consts = Proof_Context.consts_of ctxt; |
187 |
val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); |
|
188 |
val _ = length Ts <> n andalso |
|
189 |
error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ |
|
190 |
quote c ^ enclose "(" ")" (commas (replicate n "_"))); |
|
191 |
val const = Const (c, Consts.instance consts (c, Ts)); |
|
53171 | 192 |
in ML_Syntax.atomic (ML_Syntax.print_term const) end))); |
27340 | 193 |
|
46948 | 194 |
|
195 |
(* outer syntax *) |
|
196 |
||
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46948
diff
changeset
|
197 |
fun with_keyword f = |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46948
diff
changeset
|
198 |
Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) => |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
47815
diff
changeset
|
199 |
(f ((name, Thy_Header.the_keyword thy name), pos) |
48992 | 200 |
handle ERROR msg => error (msg ^ Position.here pos))); |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46948
diff
changeset
|
201 |
|
53171 | 202 |
val _ = Theory.setup |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46948
diff
changeset
|
203 |
(value (Binding.name "keyword") |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46948
diff
changeset
|
204 |
(with_keyword |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
47815
diff
changeset
|
205 |
(fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name |
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
47815
diff
changeset
|
206 |
| ((name, SOME _), pos) => |
48992 | 207 |
error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #> |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46948
diff
changeset
|
208 |
value (Binding.name "command_spec") |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46948
diff
changeset
|
209 |
(with_keyword |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
47815
diff
changeset
|
210 |
(fn ((name, SOME kind), pos) => |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46948
diff
changeset
|
211 |
"Keyword.command_spec " ^ ML_Syntax.atomic |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
47815
diff
changeset
|
212 |
((ML_Syntax.print_pair |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46948
diff
changeset
|
213 |
(ML_Syntax.print_pair ML_Syntax.print_string |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48781
diff
changeset
|
214 |
(ML_Syntax.print_pair |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48781
diff
changeset
|
215 |
(ML_Syntax.print_pair ML_Syntax.print_string |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48781
diff
changeset
|
216 |
(ML_Syntax.print_list ML_Syntax.print_string)) |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
47815
diff
changeset
|
217 |
(ML_Syntax.print_list ML_Syntax.print_string))) |
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
47815
diff
changeset
|
218 |
ML_Syntax.print_position) ((name, kind), pos)) |
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
47815
diff
changeset
|
219 |
| ((name, NONE), pos) => |
53171 | 220 |
error ("Expected command keyword " ^ quote name ^ Position.here pos)))); |
46948 | 221 |
|
27340 | 222 |
end; |
223 |