added commit_exit;
authorwenzelm
Mon Jul 14 17:51:39 2008 +0200 (2008-07-14)
changeset 2757310ba0d7d94e0
parent 27572 67cd6ed76446
child 27574 4adce8310643
added commit_exit;
src/Pure/Isar/isar.ML
     1.1 --- a/src/Pure/Isar/isar.ML	Mon Jul 14 17:47:18 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar.ML	Mon Jul 14 17:51:39 2008 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    val print: unit -> unit
     1.5    val >> : Toplevel.transition -> bool
     1.6    val >>> : Toplevel.transition list -> unit
     1.7 +  val commit_exit: unit -> unit
     1.8    val linear_undo: int -> unit
     1.9    val undo: int -> unit
    1.10    val kill: unit -> unit
    1.11 @@ -166,6 +167,19 @@
    1.12  fun print () = Toplevel.print_state false (state ());
    1.13  
    1.14  
    1.15 +(* commit final exit *)
    1.16 +
    1.17 +fun commit_exit () =
    1.18 +  let val (id, (st, _)) = point_result () in
    1.19 +    (case (Toplevel.is_toplevel st, prev_command id) of
    1.20 +      (true, SOME prev) =>
    1.21 +        (case Toplevel.transition true Toplevel.commit_exit (#1 (the_result prev)) of
    1.22 +          SOME (_, SOME (exn, msg)) => raise Exn.EXCEPTIONS ([exn], msg)
    1.23 +        | _ => ())
    1.24 +    | _ => error "Expected to find finished theory")
    1.25 +  end;
    1.26 +
    1.27 +
    1.28  (* interactive state transformations --- NOT THREAD-SAFE! *)
    1.29  
    1.30  nonfix >> >>>;