# HG changeset patch
# User wenzelm
# Date 1137702146 -3600
# Node ID 54693225c2f45e132ba3e9753017e87adc9f96ab
# Parent  dd1ebba121511d8c097094eecc4fe98b5af9e4aa
use/use_thy: Output.toplevel_errors;

diff -r dd1ebba12151 -r 54693225c2f4 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Jan 19 21:22:25 2006 +0100
+++ b/src/Pure/Thy/thy_info.ML	Thu Jan 19 21:22:26 2006 +0100
@@ -265,7 +265,7 @@
 
 in
 
-fun load_file time path =
+fun load_file time path = Output.toplevel_errors (fn () =>
   if time then
     let val name = Path.pack path in
       timeit (fn () =>
@@ -273,7 +273,7 @@
         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.unpack;
 val time_use = load_file true o Path.unpack;
@@ -375,9 +375,9 @@
       in (visited', (result, name)) end
   end;
 
-fun gen_use_thy' req prfx s =
+fun gen_use_thy' req prfx s = Output.toplevel_errors (fn () =>
   let val (_, (_, name)) = req [] prfx ([], s)
-  in Context.context (get_theory name) end;
+  in Context.context (get_theory name) end) ();
 
 fun gen_use_thy req = gen_use_thy' req Path.current;