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