minor internal changes;
authorwenzelm
Fri Dec 09 16:44:31 1994 +0100 (1994-12-09)
changeset 777c007eba368b7
parent 776 df8f91c0e57c
child 778 9a03ed31ea2f
minor internal changes;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Dec 09 16:42:09 1994 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Dec 09 16:44:31 1994 +0100
     1.3 @@ -250,8 +250,7 @@
     1.4  val type_decl = type_args -- name -- optional ("=" $$-- !! string >> Some) None
     1.5    -- opt_infix >> mk_type_decl;
     1.6  
     1.7 -val type_decls = repeat1 (old_type_decl || type_decl)
     1.8 -  >> (rpair "" o mk_type_decls o flat);
     1.9 +val type_decls = repeat1 (old_type_decl || type_decl) >> (mk_type_decls o flat);
    1.10  
    1.11  
    1.12  (* consts *)
    1.13 @@ -336,7 +335,7 @@
    1.14    (name --$$ "<" -- name >> (pair "|> AxClass.add_inst_subclass" o mk_pair) ||
    1.15      name --$$ "::" -- arity >> (pair "|> AxClass.add_inst_arity" o mk_triple2))
    1.16    -- opt_witness
    1.17 -  >> (fn ((x, y), z) => (cat_lines [x, y, z], ""));
    1.18 +  >> (fn ((x, y), z) => (cat_lines [x, y, z]));
    1.19  
    1.20  
    1.21  
    1.22 @@ -403,7 +402,8 @@
    1.23          \\n"
    1.24          ^ mltxt ^ "\n\
    1.25          \\n\
    1.26 -        \val thy = thy\n\n\
    1.27 +        \val thy = thy\n\
    1.28 +        \\n\
    1.29          \|> add_trfuns\n"
    1.30          ^ trfun_args ^ "\n\
    1.31          \\n"
    1.32 @@ -411,21 +411,24 @@
    1.33          \\n\
    1.34          \|> add_thyname " ^ quote thy_name ^ ";\n\
    1.35          \\n\
    1.36 +        \val () = store_theory (thy, " ^ quote thy_name ^ ");\n\
    1.37 +        \\n\
    1.38          \\n"
    1.39          ^ postxt ^ "\n\
    1.40          \\n\
    1.41          \end;\n\
    1.42 -        \end;\n\n\
    1.43 -        \store_theory (" ^ thy_name ^ ".thy, " ^ quote thy_name ^ ");\n"
    1.44 +        \end;\n"
    1.45      | None =>
    1.46 -        "val thy = " ^ old_thys ^ " false;\n\n\
    1.47 +        "val thy = " ^ old_thys ^ " false;\n\
    1.48 +        \\n\
    1.49          \structure " ^ thy_name ^ " =\n\
    1.50          \struct\n\
    1.51          \\n\
    1.52          \val thy = thy\n\
    1.53          \\n\
    1.54 -        \end;\n\n\
    1.55 -        \store_theory (" ^ thy_name ^ ".thy, " ^ quote thy_name ^ ");\n");
    1.56 +        \val () = store_theory (thy, " ^ quote thy_name ^ ");\n\
    1.57 +        \\n\
    1.58 +        \end;\n");
    1.59  
    1.60  fun theory_defn sectab tname =
    1.61    header -- optional (extension sectab >> Some) None -- eof
    1.62 @@ -438,9 +441,10 @@
    1.63  (* standard sections *)
    1.64  
    1.65  fun mk_val ax = "val " ^ ax ^ " = get_axiom thy " ^ quote ax ^ ";";
    1.66 +val mk_vals = cat_lines o map mk_val;
    1.67  
    1.68 -fun mk_axm_sect pretxt (txt, axs) =
    1.69 -  (pretxt ^ "\n" ^ txt, cat_lines (map mk_val axs));
    1.70 +fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs)
    1.71 +  | mk_axm_sect pretxt (txt, axs) = (pretxt ^ "\n" ^ txt, mk_vals axs);
    1.72  
    1.73  fun axm_section name pretxt parse =
    1.74    (name, parse >> mk_axm_sect pretxt);
    1.75 @@ -451,22 +455,22 @@
    1.76  
    1.77  val pure_keywords =
    1.78   ["end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+", ",", "<",
    1.79 -   "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
    1.80 +  "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
    1.81  
    1.82  val pure_sections =
    1.83   [section "classes" "|> add_classes" class_decls,
    1.84    section "default" "|> add_defsort" sort,
    1.85 -  ("types", type_decls),
    1.86 +  section "types" "" type_decls,
    1.87    section "arities" "|> add_arities" arity_decls,
    1.88    section "consts" "|> add_consts" const_decls,
    1.89    section "syntax" "|> add_syntax" const_decls,
    1.90    section "translations" "|> add_trrules" trans_decls,
    1.91    section "MLtrans" "|> add_trfuns" mltrans,
    1.92 -  ("MLtext", verbatim >> rpair ""),
    1.93 +  section "MLtext" "" verbatim,
    1.94    axm_section "rules" "|> add_axioms" axiom_decls,
    1.95    axm_section "defs" "|> add_defs" axiom_decls,
    1.96    axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
    1.97 -  ("instance", instance_decl)];
    1.98 +  section "instance" "" instance_decl];
    1.99  
   1.100  
   1.101  end;