# HG changeset patch
# User wenzelm
# Date 932669606 -7200
# Node ID e992884b256d0bc09f42c5d0895cfabd430340cc
# Parent  69d42b56151fd073a30b9e6b6797682d1baf6777
Toplevel.excursion_error;

diff -r 69d42b56151f -r e992884b256d src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Jul 22 20:52:58 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Jul 22 20:53:26 1999 +0200
@@ -295,7 +295,7 @@
     val tr_name = if time then "time_use" else "use";
   in
     if not ml orelse is_none (ThyLoad.check_file path) then ()
-    else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
+    else Toplevel.excursion_error [Toplevel.empty |> Toplevel.name tr_name |> tr]
   end;
 
 fun parse_thy (src, pos) =
@@ -323,8 +323,7 @@
   let val (src, pos) = File.source path in
     Present.theory_source name src;
     if is_old_theory (src, pos) then ThySyn.load_thy name (Source.exhaust src)
-    else (Toplevel.excursion (parse_thy (src, pos))
-      handle exn => error (Toplevel.exn_message exn))
+    else Toplevel.excursion_error (parse_thy (src, pos))
   end;
 
 fun load_thy name ml time path =
diff -r 69d42b56151f -r e992884b256d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Jul 22 20:52:58 1999 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Jul 22 20:53:26 1999 +0200
@@ -49,6 +49,7 @@
   val exn_message: exn -> string
   val apply: bool -> transition -> state -> (state * (exn * string) option) option
   val excursion: transition list -> unit
+  val excursion_error: transition list -> unit
   val set_state: state -> unit
   val get_state: unit -> state
   val exn: unit -> (exn * string) option
@@ -403,6 +404,9 @@
     State [] => ()
   | _ => raise ERROR_MESSAGE "Open block(s) pending at end of input");
 
+fun excursion_error trs =
+  excursion trs handle exn => error (exn_message exn);
+
 end;