src/Pure/Thy/thy_info.ML

 *)
 
 signature BASIC_THY_INFO =
 sig
   val theory: string -> theory
-(*val use: string -> unit*)             (*exported later*)
-  val time_use: string -> unit
   val touch_thy: string -> unit
-  val use_thy: string -> unit
-  val use_thys: string list -> unit
-  val update_thy: string -> unit
   val remove_thy: string -> unit
-  val time_use_thy: string -> unit
 end;
 
 signature THY_INFO =
 sig
   include BASIC_THY_INFO

   val loaded_files: string -> Path.T list
   val touch_child_thys: string -> unit
   val touch_all_thys: unit -> unit
   val load_file: bool -> Path.T -> unit
   val use: string -> unit
+  val time_use: string -> unit
   val pretend_use_thy_only: string -> unit
+  val use_thys: string list -> unit
+  val use_thy: string -> unit
+  val time_use_thy: string -> unit
+  val update_thy: string -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
   val end_theory: theory -> theory
   val finish: unit -> unit
   val register_theory: theory -> unit
   val pretty_theory: theory -> Pretty.T

           change_deps name (provide path name (ThyLoad.load_ml (master_dir' deps) path))
       | NONE => (ThyLoad.load_ml Path.current path; ())));
 
 in
 
-fun load_file time path = Output.toplevel_errors (fn () =>
+fun load_file time path =
   if time then
     let val name = Path.implode path in
       timeit (fn () =>
        (priority ("\n**** Starting file " ^ quote name ^ " ****");
         run_file path;
         priority ("**** Finished file " ^ quote name ^ " ****\n")))
     end
-  else run_file path) ();
+  else run_file path;
 
 val use = load_file false o Path.explode;
 val time_use = load_file true o Path.explode;
 
 end;

       (case Multithreading.schedule (Int.min (m, n)) next_task tasks of
         [] => ()
       | exns => raise Exn.EXCEPTIONS (exns, ""))
   end;
 
-fun gen_use_thy' req dir arg = Output.toplevel_errors (fn () =>
+fun gen_use_thy' req dir arg =
   let val (_, tasks) = req [] dir arg (Graph.empty, 0)
-  in schedule_tasks tasks end) ();
+  in schedule_tasks tasks end;
 
 fun gen_use_thy req str =
   let val name = base_name str in
     check_unfinished warning name;
     gen_use_thy' req Path.current str;