src/Pure/Isar/outer_syntax.ML

--- a/src/Pure/Isar/outer_syntax.ML	Sat Jan 14 17:14:16 2006 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Jan 14 17:14:17 2006 +0100
@@ -15,6 +15,7 @@
       val loop: unit -> unit
       val sync_main: unit -> unit
       val sync_loop: unit -> unit
+      val toplevel: (unit -> 'a) -> 'a
     end;
 end;
 
@@ -271,7 +272,7 @@
     else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
   end;
 
-fun run_thy name path =
+fun run_thy name path = Output.toplevel_errors (fn () =>
   let
     val text = Source.of_list (Library.untabify (explode (File.read path)));
     val _ = Present.init_theory name;
@@ -287,7 +288,7 @@
     IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
     |> Buffer.content
     |> Present.theory_output name
-  end;
+  end) ();
 
 in
 
@@ -327,6 +328,7 @@
   fun loop () = gen_loop false false;
   fun sync_main () = gen_main true true;
   fun sync_loop () = gen_loop true true;
+  val toplevel = Toplevel.program;
 end;