src/Pure/Thy/thy_info.ML
changeset 6329 bbd03b119f36
parent 6263 f30d1e31b9df
child 6362 bbbea7fecb93
     1.1 --- a/src/Pure/Thy/thy_info.ML	Tue Mar 09 12:18:02 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Mar 09 12:18:46 1999 +0100
     1.3 @@ -40,9 +40,10 @@
     1.4    val put_theory: theory -> unit
     1.5    val loaded_files: string -> (Path.T * File.info) list
     1.6    val load_file: bool -> Path.T -> unit
     1.7 +  val use_path: Path.T -> unit
     1.8    val use: string -> unit
     1.9    val use_thy_only: string -> unit
    1.10 -  val begin_theory: string -> string list -> theory
    1.11 +  val begin_theory: string -> string list -> (Path.T * bool) list -> theory
    1.12    val end_theory: theory -> theory
    1.13    val finalize_all: unit -> unit
    1.14    val register_theory: theory -> unit
    1.15 @@ -248,7 +249,8 @@
    1.16            writeln ("**** Finished file " ^ quote name ^ " ****\n")))
    1.17        end;
    1.18  
    1.19 -val use = load_file false o Path.unpack;
    1.20 +val use_path = load_file false;
    1.21 +val use = use_path o Path.unpack;
    1.22  val time_use = load_file true o Path.unpack;
    1.23  
    1.24  
    1.25 @@ -306,14 +308,15 @@
    1.26  val use_thy_only = gen_use_thy (require_thy false false true false []);
    1.27  
    1.28  
    1.29 -(* begin / end theory *)                (* FIXME tune *)
    1.30 +(* begin / end theory *)                (* FIXME tune *) (* FIXME files vs. paths (!?!?) *)
    1.31  
    1.32 -fun begin_theory name parents =
    1.33 +fun begin_theory name parents paths =
    1.34    let
    1.35      val _ = seq weak_use_thy parents;
    1.36      val theory = PureThy.begin_theory name (map get_theory parents);
    1.37      val _ = change_thys (update_node name parents (init_deps [] [], Some (theory, Symtab.empty)));
    1.38 -  in theory end;
    1.39 +    val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
    1.40 +  in Context.setmp (Some theory) (seq use_path) use_paths; theory end;
    1.41  
    1.42  fun end_theory theory =
    1.43    let val theory' = PureThy.end_theory theory