228 [(mk_triple (t, string_of_int (length xs), syn), false)] |
227 [(mk_triple (t, string_of_int (length xs), syn), false)] |
229 | mk_type_decl (((xs, t), Some rhs), syn) = |
228 | mk_type_decl (((xs, t), Some rhs), syn) = |
230 [(pars (commas [t, mk_list xs, rhs, syn]), true)]; |
229 [(pars (commas [t, mk_list xs, rhs, syn]), true)]; |
231 |
230 |
232 fun mk_type_decls tys = |
231 fun mk_type_decls tys = |
233 "also add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\ |
232 "|> add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\ |
234 \also add_tyabbrs\n" ^ mk_big_list (keyfilter tys true); |
233 \|> add_tyabbrs\n" ^ mk_big_list (keyfilter tys true); |
235 |
234 |
236 |
235 |
237 val old_type_decl = names -- nat -- opt_infix >> mk_old_type_decl; |
236 val old_type_decl = names -- nat -- opt_infix >> mk_old_type_decl; |
238 |
237 |
239 val type_args = |
238 val type_args = |
307 (strip_quotes c ^ "I") :: map fst axms); |
306 (strip_quotes c ^ "I") :: map fst axms); |
308 |
307 |
309 val axclass_decl = subclass -- repeat (ident -- !! string) >> mk_axclass_decl; |
308 val axclass_decl = subclass -- repeat (ident -- !! string) >> mk_axclass_decl; |
310 |
309 |
311 |
310 |
|
311 (* sigclass *) |
|
312 |
|
313 fun mk_sigclass_decl ((c, cs), consts) = |
|
314 (mk_pair (c, cs) ^ "\n" ^ consts, [strip_quotes c ^ "I"]); |
|
315 |
|
316 val sigclass_decl = subclass -- optional const_decls "[]" >> mk_sigclass_decl; |
|
317 |
|
318 |
312 (* instance *) |
319 (* instance *) |
313 |
320 |
314 fun mk_instance_decl ((((t, ss), c), axths), opt_tac) = |
321 fun mk_instance_decl ((((t, ss), c), axths), opt_tac) = |
315 mk_triple (t, ss, c) ^ "\n" ^ |
322 mk_triple (t, ss, c) ^ "\n" ^ |
316 mk_list (keyfilter axths false) ^ "\n" ^ |
323 mk_list (keyfilter axths false) ^ "\n" ^ |
428 |
435 |
429 |
436 |
430 val pure_keywords = |
437 val pure_keywords = |
431 ["classes", "default", "types", "arities", "consts", "syntax", |
438 ["classes", "default", "types", "arities", "consts", "syntax", |
432 "translations", "MLtrans", "MLtext", "rules", "defns", "axclass", |
439 "translations", "MLtrans", "MLtext", "rules", "defns", "axclass", |
433 "instance", "end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+", |
440 "sigclass", "instance", "end", "ML", "mixfix", "infixr", "infixl", |
434 ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="]; |
441 "binder", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", |
|
442 "==", "=>", "<="]; |
435 |
443 |
436 val pure_sections = |
444 val pure_sections = |
437 [section "classes" "also add_classes" class_decls, |
445 [section "classes" "|> add_classes" class_decls, |
438 section "default" "also add_defsort" sort, |
446 section "default" "|> add_defsort" sort, |
439 ("types", type_decls), |
447 ("types", type_decls), |
440 section "arities" "also add_arities" arity_decls, |
448 section "arities" "|> add_arities" arity_decls, |
441 section "consts" "also add_consts" const_decls, |
449 section "consts" "|> add_consts" const_decls, |
442 section "syntax" "also add_syntax" const_decls, |
450 section "syntax" "|> add_syntax" const_decls, |
443 section "translations" "also add_trrules" trans_decls, |
451 section "translations" "|> add_trrules" trans_decls, |
444 section "MLtrans" "also add_trfuns" mltrans, |
452 section "MLtrans" "|> add_trfuns" mltrans, |
445 ("MLtext", verbatim >> rpair ""), |
453 ("MLtext", verbatim >> rpair ""), |
446 axm_section "rules" "also add_axioms" axiom_decls, |
454 axm_section "rules" "|> add_axioms" axiom_decls, |
447 axm_section "defns" "also add_defns" axiom_decls, |
455 axm_section "defns" "|> add_defns" axiom_decls, |
448 axm_section "axclass" "also add_axclass" axclass_decl, |
456 axm_section "axclass" "|> add_axclass" axclass_decl, |
449 section "instance" "also add_instance" instance_decl]; |
457 axm_section "sigclass" "|> add_sigclass" sigclass_decl, |
450 |
458 section "instance" "|> add_instance" instance_decl]; |
451 |
459 |
452 (* FIXME -> thy_read.ML *) |
|
453 val pure_syntax = make_syntax pure_keywords pure_sections; |
|
454 |
460 |
455 end; |
461 end; |
456 |
462 |