replaced thy_setup by 'setup' section;
authorwenzelm
Wed Apr 29 11:26:59 1998 +0200 (1998-04-29)
changeset 485258b5006d36cc
parent 4851 cbbc53963aaa
child 4853 67bcbb03c235
replaced thy_setup by 'setup' section;
adapted to new PureThy.add_axioms / PureThy.add_defs;
added 'nonterminals' section;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Apr 29 11:25:26 1998 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Apr 29 11:26:59 1998 +0200
     1.3 @@ -344,8 +344,7 @@
     1.4    \ val print_translation = [];\n\
     1.5    \ val typed_print_translation = [];\n\
     1.6    \ val print_ast_translation = [];\n\
     1.7 -  \ val token_translation = [];\n\
     1.8 -  \ val thy_setup = []";
     1.9 +  \ val token_translation = [];";
    1.10  
    1.11  val trfun_args =
    1.12    "(parse_ast_translation, parse_translation, \
    1.13 @@ -373,7 +372,7 @@
    1.14      val (axms_defs, axms_names) =
    1.15        mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
    1.16    in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
    1.17 -       "\n\n|> PureThy.add_store_defs\n" ^ axms_defs, axms_names)
    1.18 +       "\n\n|> (PureThy.add_defs o map Attribute.none)\n" ^ axms_defs, axms_names)
    1.19    end;
    1.20  
    1.21  val constaxiom_decls =
    1.22 @@ -419,7 +418,7 @@
    1.23  fun empty_decl toks = (empty >> K "") toks;
    1.24  
    1.25  val global_path =
    1.26 -  "|> (fn thy => if ! global_names then thy else Theory.add_path \"/\" thy)";
    1.27 +  "|> (fn thy => if ! global_names then thy else Theory.root_path thy)";
    1.28  
    1.29  val local_path =
    1.30    global_path ^ "\n\
    1.31 @@ -503,7 +502,6 @@
    1.32      \\n"
    1.33      ^ local_path ^
    1.34      "\n\
    1.35 -    \|> Theory.setup thy_setup\n\
    1.36      \|> Theory.add_trfuns\n"
    1.37      ^ trfun_args ^ "\n\
    1.38      \|> Theory.add_trfunsT typed_print_translation\n\
    1.39 @@ -556,12 +554,13 @@
    1.40   [section "classes" "|> Theory.add_classes" class_decls,
    1.41    section "default" "|> Theory.add_defsort" sort,
    1.42    section "types" "" type_decls,
    1.43 +  section "nonterminals" "|> Theory.add_nonterminals" (repeat1 name >> mk_list),
    1.44    section "arities" "|> Theory.add_arities" arity_decls,
    1.45    section "consts" "|> Theory.add_consts" const_decls,
    1.46    section "syntax" "|> Theory.add_modesyntax" syntax_decls,
    1.47    section "translations" "|> Theory.add_trrules" trans_decls,
    1.48 -  axm_section "rules" "|> PureThy.add_store_axioms" axiom_decls,
    1.49 -  axm_section "defs" "|> PureThy.add_store_defs" axiom_decls,
    1.50 +  axm_section "rules" "|> (PureThy.add_axioms o map Attribute.none)" axiom_decls,
    1.51 +  axm_section "defs" "|> (PureThy.add_defs o map Attribute.none)" axiom_decls,
    1.52    section "oracle" "|> Theory.add_oracle" oracle_decl,
    1.53    axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
    1.54    axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
    1.55 @@ -569,6 +568,7 @@
    1.56    section "path" "|> Theory.add_path" name,
    1.57    section "global" global_path empty_decl,
    1.58    section "local" local_path empty_decl,
    1.59 +  section "setup" "|> Theory.apply" long_id,
    1.60    section "MLtext" "" verbatim];
    1.61  
    1.62