# HG changeset patch
# User wenzelm
# Date 940957526 -7200
# Node ID cbeaff0ef8562fd6be04c527a7a4098c71780e05
# Parent  ac62465ed06cbf2028e8d847cf44875547ef5ba3
added kill_proof_notify;

diff -r ac62465ed06c -r cbeaff0ef856 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Oct 26 19:04:55 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 26 19:05:26 1999 +0200
@@ -20,6 +20,7 @@
   val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
   val redo: Toplevel.transition -> Toplevel.transition
   val undos_proof: int -> Toplevel.transition -> Toplevel.transition
+  val kill_proof_notify: (unit -> unit) -> Toplevel.transition -> Toplevel.transition
   val kill_proof: Toplevel.transition -> Toplevel.transition
   val undo_theory: Toplevel.transition -> Toplevel.transition
   val undo: Toplevel.transition -> Toplevel.transition
@@ -84,10 +85,12 @@
 fun undos_proof n = Toplevel.proof (fn prf =>
   if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf);
 
-val kill_proof = Toplevel.history (fn hist =>
+fun kill_proof_notify (f: unit -> unit) = Toplevel.history (fn hist =>
   (case History.current hist of
     Toplevel.Theory _ => raise Toplevel.UNDEF
-  | Toplevel.Proof _ => History.undo hist));
+  | Toplevel.Proof _ => (f (); History.undo hist)));
+
+val kill_proof = kill_proof_notify (K ());
 
 val undo_theory = Toplevel.history (fn hist =>
   if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);