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