--- a/src/Pure/Isar/isar.ML Mon Jul 14 17:47:18 2008 +0200
+++ b/src/Pure/Isar/isar.ML Mon Jul 14 17:51:39 2008 +0200
@@ -15,6 +15,7 @@
val print: unit -> unit
val >> : Toplevel.transition -> bool
val >>> : Toplevel.transition list -> unit
+ val commit_exit: unit -> unit
val linear_undo: int -> unit
val undo: int -> unit
val kill: unit -> unit
@@ -166,6 +167,19 @@
fun print () = Toplevel.print_state false (state ());
+(* commit final exit *)
+
+fun commit_exit () =
+ let val (id, (st, _)) = point_result () in
+ (case (Toplevel.is_toplevel st, prev_command id) of
+ (true, SOME prev) =>
+ (case Toplevel.transition true Toplevel.commit_exit (#1 (the_result prev)) of
+ SOME (_, SOME (exn, msg)) => raise Exn.EXCEPTIONS ([exn], msg)
+ | _ => ())
+ | _ => error "Expected to find finished theory")
+ end;
+
+
(* interactive state transformations --- NOT THREAD-SAFE! *)
nonfix >> >>>;