src/Pure/Thy/thy_info.ML

   val names: unit -> string list
   val get_theory: string -> theory
   val put_theory: theory -> unit
   val loaded_files: string -> (Path.T * File.info) list
   val load_file: bool -> Path.T -> unit
+  val use_path: Path.T -> unit
   val use: string -> unit
   val use_thy_only: string -> unit
-  val begin_theory: string -> string list -> theory
+  val begin_theory: string -> string list -> (Path.T * bool) list -> theory
   val end_theory: theory -> theory
   val finalize_all: unit -> unit
   val register_theory: theory -> unit
 end;
 

          (writeln ("\n**** Starting file " ^ quote name ^ " ****");
           run_file path;
           writeln ("**** Finished file " ^ quote name ^ " ****\n")))
       end;
 
-val use = load_file false o Path.unpack;
+val use_path = load_file false;
+val use = use_path o Path.unpack;
 val time_use = load_file true o Path.unpack;
 
 
 (* require_thy *)
 

 val update_thy   = gen_use_thy (require_thy true false true true []);
 val time_use_thy = gen_use_thy (require_thy true true true false []);
 val use_thy_only = gen_use_thy (require_thy false false true false []);
 
 
-(* begin / end theory *)                (* FIXME tune *)
-
-fun begin_theory name parents =
+(* begin / end theory *)                (* FIXME tune *) (* FIXME files vs. paths (!?!?) *)
+
+fun begin_theory name parents paths =
   let
     val _ = seq weak_use_thy parents;
     val theory = PureThy.begin_theory name (map get_theory parents);
     val _ = change_thys (update_node name parents (init_deps [] [], Some (theory, Symtab.empty)));
-  in theory end;
+    val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
+  in Context.setmp (Some theory) (seq use_path) use_paths; theory end;
 
 fun end_theory theory =
   let val theory' = PureThy.end_theory theory
   in put_theory theory'; theory' end;