# HG changeset patch
# User wenzelm
# Date 1137255257 -3600
# Node ID 38d72231b41d890759cc8812b25f55a8ff8c6460
# Parent  a8f9c192f6d1d81c825e0e326c6855bdeff62a18
added Isar.toplevel;

diff -r a8f9c192f6d1 -r 38d72231b41d 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;