renamed base_on into mk_base and moved it to the beginning of the generated
authorclasohm
Tue Sep 06 14:44:10 1994 +0200 (1994-09-06)
changeset 586201e115d8031
parent 585 409c9ee7a9f3
child 587 3ba470399605
renamed base_on into mk_base and moved it to the beginning of the generated
.thy.ML file to make sure that all base theories are present when ML executes
the rest of this file
src/Pure/Thy/thy_parse.ML
src/Pure/Thy/thy_read.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Sep 06 13:46:53 1994 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Sep 06 14:44:10 1994 +0200
     1.3 @@ -350,7 +350,7 @@
     1.4  (* header *)
     1.5  
     1.6  fun mk_header (thy_name, bases) =
     1.7 -  (thy_name, "base_on " ^ mk_list bases ^ " " ^ quote thy_name);
     1.8 +  (thy_name, "mk_base " ^ mk_list bases ^ " " ^ quote thy_name);
     1.9  
    1.10  val base =
    1.11    ident >> (cat "Thy" o quote) ||
    1.12 @@ -389,7 +389,8 @@
    1.13    else
    1.14      (case opt_txts of
    1.15        Some (extxt, postxt, mltxt) =>
    1.16 -        "structure " ^ thy_name ^ " =\n\
    1.17 +        "val base = " ^ old_thys ^ " true;\n\n\
    1.18 +        \structure " ^ thy_name ^ " =\n\
    1.19          \struct\n\
    1.20          \\n\
    1.21          \local\n"
    1.22 @@ -398,7 +399,7 @@
    1.23          \\n"
    1.24          ^ mltxt ^ "\n\
    1.25          \\n\
    1.26 -        \val thy = (" ^ old_thys ^ " true)\n\n\
    1.27 +        \val thy = base\n\n\
    1.28          \|> add_trfuns\n"
    1.29          ^ trfun_args ^ "\n\
    1.30          \\n"
    1.31 @@ -412,10 +413,11 @@
    1.32          \end;\n\
    1.33          \end;\n"
    1.34      | None =>
    1.35 -        "structure " ^ thy_name ^ " =\n\
    1.36 +        "val base = " ^ old_thys ^ " false;\n\n\
    1.37 +        \structure " ^ thy_name ^ " =\n\
    1.38          \struct\n\
    1.39          \\n\
    1.40 -        \val thy = (" ^ old_thys ^ " false);\n\
    1.41 +        \val thy = base\n\
    1.42          \\n\
    1.43          \end;\n");
    1.44  
     2.1 --- a/src/Pure/Thy/thy_read.ML	Tue Sep 06 13:46:53 1994 +0200
     2.2 +++ b/src/Pure/Thy/thy_read.ML	Tue Sep 06 14:44:10 1994 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4    val update         : unit -> unit
     2.5    val time_use_thy   : string -> unit
     2.6    val unlink_thy     : string -> unit
     2.7 -  val base_on        : basetype list -> string -> bool -> theory
     2.8 +  val mk_base        : basetype list -> string -> bool -> theory
     2.9    val store_theory   : theory * string -> unit
    2.10  
    2.11    val theory_of_sign: Sign.sg -> theory
    2.12 @@ -333,7 +333,7 @@
    2.13  
    2.14  (*Merge theories to build a base for a new theory.
    2.15    Base members are only loaded if they are missing. *)
    2.16 -fun base_on bases child mk_draft =
    2.17 +fun mk_base bases child mk_draft =
    2.18        let (*List all descendants of a theory list *)
    2.19            fun list_descendants (t :: ts) =
    2.20                  let val tinfo = get_thyinfo t