src/Pure/Isar/toplevel.ML

   val is_init: transition -> bool
   val modify_init: (unit -> theory) -> transition -> transition
   val exit: transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
+  val keep_proof: (state -> unit) -> transition -> transition
   val ignored: Position.T -> transition
   val is_ignored: transition -> bool
   val malformed: Position.T -> string -> transition
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition

 fun present_transaction f g = add_trans (Transaction (f, g));
 fun transaction f = present_transaction f (K ());
 
 fun keep f = add_trans (Keep (fn _ => f));
 
+fun keep_proof f =
+  keep (fn st =>
+    if is_proof st then f st
+    else if is_skipped_proof st then ()
+    else warning "No proof state");
+
 fun ignored pos = empty |> name "<ignored>" |> position pos |> keep (fn _ => ());
 fun is_ignored tr = name_of tr = "<ignored>";
 
 fun malformed pos msg =
   empty |> name "<malformed>" |> position pos |> keep (fn _ => error msg);