src/Pure/Thy/thy_parse.ML
changeset 3764 fe7719aee219
parent 3528 f4b28e25ba99
child 3770 294b5905f4eb
equal deleted inserted replaced
3763:31ec17820f49 3764:fe7719aee219
   277       [(mk_triple (t, string_of_int (length xs), syn), false)]
   277       [(mk_triple (t, string_of_int (length xs), syn), false)]
   278   | mk_type_decl (((xs, t), Some rhs), syn) =
   278   | mk_type_decl (((xs, t), Some rhs), syn) =
   279       [(parens (commas [t, mk_list xs, rhs, syn]), true)];
   279       [(parens (commas [t, mk_list xs, rhs, syn]), true)];
   280 
   280 
   281 fun mk_type_decls tys =
   281 fun mk_type_decls tys =
   282   "|> add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
   282   "|> Theory.add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
   283   \|> add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
   283   \|> Theory.add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
   284 
   284 
   285 
   285 
   286 val old_type_decl = names1 -- nat -- opt_infix >> mk_old_type_decl;
   286 val old_type_decl = names1 -- nat -- opt_infix >> mk_old_type_decl;
   287 
   287 
   288 val type_args =
   288 val type_args =
   360 fun mk_constaxiom_decls x =
   360 fun mk_constaxiom_decls x =
   361   let
   361   let
   362     val (axms_defs, axms_names) =
   362     val (axms_defs, axms_names) =
   363       mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
   363       mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
   364   in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
   364   in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
   365        "\n\n|> add_defs\n" ^ axms_defs, axms_names)
   365        "\n\n|> Theory.add_defs\n" ^ axms_defs, axms_names)
   366   end;
   366   end;
   367 
   367 
   368 val constaxiom_decls =
   368 val constaxiom_decls =
   369   repeat1 (ident --$$ "::" -- !!
   369   repeat1 (ident --$$ "::" -- !!
   370            ((string || const_type false >> quote) -- opt_mixfix) -- !!
   370            ((string || const_type false >> quote) -- opt_mixfix) -- !!
   468         \\n"
   468         \\n"
   469         ^ mltxt ^ "\n\
   469         ^ mltxt ^ "\n\
   470         \\n\
   470         \\n\
   471         \val thy = thy\n\
   471         \val thy = thy\n\
   472         \\n\
   472         \\n\
   473         \|> add_trfuns\n"
   473         \|> Theory.add_trfuns\n"
   474         ^ trfun_args ^ "\n\
   474         ^ trfun_args ^ "\n\
   475         \|> add_trfunsT typed_print_translation \n\
   475         \|> Theory.add_trfunsT typed_print_translation \n\
   476         \|> add_tokentrfuns token_translation \n\
   476         \|> Theory.add_tokentrfuns token_translation \n\
   477         \\n"
   477         \\n"
   478         ^ extxt ^ "\n\
   478         ^ extxt ^ "\n\
   479         \\n\
   479         \\n\
   480         \|> add_thyname " ^ quote thy_name ^ ";\n\
   480         \|> Theory.add_name " ^ quote thy_name ^ ";\n\
   481         \\n\
   481         \\n\
   482         \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
   482         \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
   483         \\n\
   483         \\n\
   484         \\n"
   484         \\n"
   485         ^ postxt ^ "\n\
   485         ^ postxt ^ "\n\
   532  ["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=",
   532  ["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=",
   533   "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
   533   "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
   534 
   534 
   535 val pure_sections =
   535 val pure_sections =
   536  [section "oracle" "|> set_oracle" (name >> strip_quotes),
   536  [section "oracle" "|> set_oracle" (name >> strip_quotes),
   537   section "classes" "|> add_classes" class_decls,
   537   section "classes" "|> Theory.add_classes" class_decls,
   538   section "default" "|> add_defsort" sort,
   538   section "default" "|> Theory.add_defsort" sort,
   539   section "types" "" type_decls,
   539   section "types" "" type_decls,
   540   section "arities" "|> add_arities" arity_decls,
   540   section "arities" "|> Theory.add_arities" arity_decls,
   541   section "consts" "|> add_consts" const_decls,
   541   section "consts" "|> Theory.add_consts" const_decls,
   542   section "syntax" "|> add_modesyntax" syntax_decls,
   542   section "syntax" "|> Theory.add_modesyntax" syntax_decls,
   543   section "translations" "|> add_trrules" trans_decls,
   543   section "translations" "|> Theory.add_trrules" trans_decls,
   544   axm_section "rules" "|> add_axioms" axiom_decls,
   544   axm_section "rules" "|> Theory.add_axioms" axiom_decls,
   545   axm_section "defs" "|> add_defs" axiom_decls,
   545   axm_section "defs" "|> Theory.add_defs" axiom_decls,
   546   axm_section "constdefs" "|> add_consts" constaxiom_decls,
   546   axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
   547   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   547   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   548   section "instance" "" instance_decl];
   548   section "instance" "" instance_decl];
   549 
   549 
   550 end;
   550 end;