401 ^ trfun_defs ^ "\n\ |
400 ^ trfun_defs ^ "\n\ |
402 \in\n\ |
401 \in\n\ |
403 \\n" |
402 \\n" |
404 ^ mltxt ^ "\n\ |
403 ^ mltxt ^ "\n\ |
405 \\n\ |
404 \\n\ |
406 \val thy = thy\n\n\ |
405 \val thy = thy\n\ |
|
406 \\n\ |
407 \|> add_trfuns\n" |
407 \|> add_trfuns\n" |
408 ^ trfun_args ^ "\n\ |
408 ^ trfun_args ^ "\n\ |
409 \\n" |
409 \\n" |
410 ^ extxt ^ "\n\ |
410 ^ extxt ^ "\n\ |
411 \\n\ |
411 \\n\ |
412 \|> add_thyname " ^ quote thy_name ^ ";\n\ |
412 \|> add_thyname " ^ quote thy_name ^ ";\n\ |
413 \\n\ |
413 \\n\ |
|
414 \val () = store_theory (thy, " ^ quote thy_name ^ ");\n\ |
|
415 \\n\ |
414 \\n" |
416 \\n" |
415 ^ postxt ^ "\n\ |
417 ^ postxt ^ "\n\ |
416 \\n\ |
418 \\n\ |
417 \end;\n\ |
419 \end;\n\ |
418 \end;\n\n\ |
420 \end;\n" |
419 \store_theory (" ^ thy_name ^ ".thy, " ^ quote thy_name ^ ");\n" |
|
420 | None => |
421 | None => |
421 "val thy = " ^ old_thys ^ " false;\n\n\ |
422 "val thy = " ^ old_thys ^ " false;\n\ |
|
423 \\n\ |
422 \structure " ^ thy_name ^ " =\n\ |
424 \structure " ^ thy_name ^ " =\n\ |
423 \struct\n\ |
425 \struct\n\ |
424 \\n\ |
426 \\n\ |
425 \val thy = thy\n\ |
427 \val thy = thy\n\ |
426 \\n\ |
428 \\n\ |
427 \end;\n\n\ |
429 \val () = store_theory (thy, " ^ quote thy_name ^ ");\n\ |
428 \store_theory (" ^ thy_name ^ ".thy, " ^ quote thy_name ^ ");\n"); |
430 \\n\ |
|
431 \end;\n"); |
429 |
432 |
430 fun theory_defn sectab tname = |
433 fun theory_defn sectab tname = |
431 header -- optional (extension sectab >> Some) None -- eof |
434 header -- optional (extension sectab >> Some) None -- eof |
432 >> (mk_structure tname o #1); |
435 >> (mk_structure tname o #1); |
433 |
436 |
436 |
439 |
437 |
440 |
438 (* standard sections *) |
441 (* standard sections *) |
439 |
442 |
440 fun mk_val ax = "val " ^ ax ^ " = get_axiom thy " ^ quote ax ^ ";"; |
443 fun mk_val ax = "val " ^ ax ^ " = get_axiom thy " ^ quote ax ^ ";"; |
441 |
444 val mk_vals = cat_lines o map mk_val; |
442 fun mk_axm_sect pretxt (txt, axs) = |
445 |
443 (pretxt ^ "\n" ^ txt, cat_lines (map mk_val axs)); |
446 fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs) |
|
447 | mk_axm_sect pretxt (txt, axs) = (pretxt ^ "\n" ^ txt, mk_vals axs); |
444 |
448 |
445 fun axm_section name pretxt parse = |
449 fun axm_section name pretxt parse = |
446 (name, parse >> mk_axm_sect pretxt); |
450 (name, parse >> mk_axm_sect pretxt); |
447 |
451 |
448 fun section name pretxt parse = |
452 fun section name pretxt parse = |
449 axm_section name pretxt (parse >> rpair []); |
453 axm_section name pretxt (parse >> rpair []); |
450 |
454 |
451 |
455 |
452 val pure_keywords = |
456 val pure_keywords = |
453 ["end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+", ",", "<", |
457 ["end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+", ",", "<", |
454 "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="]; |
458 "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="]; |
455 |
459 |
456 val pure_sections = |
460 val pure_sections = |
457 [section "classes" "|> add_classes" class_decls, |
461 [section "classes" "|> add_classes" class_decls, |
458 section "default" "|> add_defsort" sort, |
462 section "default" "|> add_defsort" sort, |
459 ("types", type_decls), |
463 section "types" "" type_decls, |
460 section "arities" "|> add_arities" arity_decls, |
464 section "arities" "|> add_arities" arity_decls, |
461 section "consts" "|> add_consts" const_decls, |
465 section "consts" "|> add_consts" const_decls, |
462 section "syntax" "|> add_syntax" const_decls, |
466 section "syntax" "|> add_syntax" const_decls, |
463 section "translations" "|> add_trrules" trans_decls, |
467 section "translations" "|> add_trrules" trans_decls, |
464 section "MLtrans" "|> add_trfuns" mltrans, |
468 section "MLtrans" "|> add_trfuns" mltrans, |
465 ("MLtext", verbatim >> rpair ""), |
469 section "MLtext" "" verbatim, |
466 axm_section "rules" "|> add_axioms" axiom_decls, |
470 axm_section "rules" "|> add_axioms" axiom_decls, |
467 axm_section "defs" "|> add_defs" axiom_decls, |
471 axm_section "defs" "|> add_defs" axiom_decls, |
468 axm_section "axclass" "|> AxClass.add_axclass" axclass_decl, |
472 axm_section "axclass" "|> AxClass.add_axclass" axclass_decl, |
469 ("instance", instance_decl)]; |
473 section "instance" "" instance_decl]; |
470 |
474 |
471 |
475 |
472 end; |
476 end; |