76 val type_const: string parser |
76 val type_const: string parser |
77 val arity: (string * string list * string) parser |
77 val arity: (string * string list * string) parser |
78 val multi_arity: (string list * string list * string) parser |
78 val multi_arity: (string list * string list * string) parser |
79 val type_args: string list parser |
79 val type_args: string list parser |
80 val type_args_constrained: (string * string option) list parser |
80 val type_args_constrained: (string * string option) list parser |
81 val typ_group: string parser |
|
82 val typ: string parser |
81 val typ: string parser |
83 val mixfix: mixfix parser |
82 val mixfix: mixfix parser |
84 val mixfix': mixfix parser |
83 val mixfix': mixfix parser |
85 val opt_mixfix: mixfix parser |
84 val opt_mixfix: mixfix parser |
86 val opt_mixfix': mixfix parser |
85 val opt_mixfix': mixfix parser |
91 val params: (binding * string option * mixfix) list parser |
90 val params: (binding * string option * mixfix) list parser |
92 val fixes: (binding * string option * mixfix) list parser |
91 val fixes: (binding * string option * mixfix) list parser |
93 val for_fixes: (binding * string option * mixfix) list parser |
92 val for_fixes: (binding * string option * mixfix) list parser |
94 val ML_source: Input.source parser |
93 val ML_source: Input.source parser |
95 val document_source: Input.source parser |
94 val document_source: Input.source parser |
96 val term_group: string parser |
95 val const: string parser |
97 val prop_group: string parser |
|
98 val term: string parser |
96 val term: string parser |
99 val prop: string parser |
97 val prop: string parser |
100 val const: string parser |
|
101 val literal_fact: string parser |
98 val literal_fact: string parser |
102 val propp: (string * string list) parser |
99 val propp: (string * string list) parser |
103 val termp: (string * string list) parser |
100 val termp: (string * string list) parser |
104 val private: Position.T parser |
101 val private: Position.T parser |
105 val qualified: Position.T parser |
102 val qualified: Position.T parser |
266 |
263 |
267 val binding = position name >> Binding.make; |
264 val binding = position name >> Binding.make; |
268 |
265 |
269 val embedded = |
266 val embedded = |
270 group (fn () => "embedded content") |
267 group (fn () => "embedded content") |
271 (short_ident || long_ident || sym_ident || number || string || cartouche); |
268 (cartouche || string || short_ident || long_ident || sym_ident || |
|
269 term_var || type_ident || type_var || number); |
272 |
270 |
273 val text = |
271 val text = |
274 group (fn () => "text") |
272 group (fn () => "text") |
275 (short_ident || long_ident || sym_ident || number || string || verbatim || cartouche); |
273 (short_ident || long_ident || sym_ident || number || string || verbatim || cartouche); |
276 |
274 |
299 (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2; |
297 (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2; |
300 |
298 |
301 |
299 |
302 (* types *) |
300 (* types *) |
303 |
301 |
304 val typ_group = |
302 val typ = group (fn () => "type") (inner_syntax embedded); |
305 group (fn () => "type") |
|
306 (short_ident || long_ident || sym_ident || type_ident || type_var || number || |
|
307 string || cartouche); |
|
308 |
|
309 val typ = inner_syntax typ_group; |
|
310 |
303 |
311 fun type_arguments arg = |
304 fun type_arguments arg = |
312 arg >> single || |
305 arg >> single || |
313 $$$ "(" |-- !!! (list1 arg --| $$$ ")") || |
306 $$$ "(" |-- !!! (list1 arg --| $$$ ")") || |
314 Scan.succeed []; |
307 Scan.succeed []; |
391 val document_source = input (group (fn () => "document source") text); |
384 val document_source = input (group (fn () => "document source") text); |
392 |
385 |
393 |
386 |
394 (* terms *) |
387 (* terms *) |
395 |
388 |
396 val term_group = group (fn () => "term") (term_var || embedded); |
|
397 val prop_group = group (fn () => "proposition") (term_var || embedded); |
|
398 |
|
399 val term = inner_syntax term_group; |
|
400 val prop = inner_syntax prop_group; |
|
401 |
|
402 val const = group (fn () => "constant") (inner_syntax embedded); |
389 val const = group (fn () => "constant") (inner_syntax embedded); |
|
390 val term = group (fn () => "term") (inner_syntax embedded); |
|
391 val prop = group (fn () => "proposition") (inner_syntax embedded); |
403 |
392 |
404 val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche)); |
393 val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche)); |
405 |
394 |
406 |
395 |
407 (* patterns *) |
396 (* patterns *) |