--- 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;