# HG changeset patch
# User wenzelm
# Date 1216050699 -7200
# Node ID 10ba0d7d94e0f5054977d9fcb9309a6b04982081
# Parent  67cd6ed76446fd880faa6a9a5fbf781c496e8f1c
added commit_exit;

diff -r 67cd6ed76446 -r 10ba0d7d94e0 src/Pure/Isar/isar.ML
--- 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 >> >>>;