Only successful proofs are ripleyed

examples/programs/isqrt.mlw

@@ -20,7 +20,7 @@ module M
 
   let main () =
     { }
-    let r = isqrt 17 in
+    let r = isqrt 42 in
     assert { r < 4 -> false };
     assert { r > 4 -> false };
     r

src/ide/gconfig.ml

@@ -218,6 +218,7 @@ let iconname_transf = "configure32"
 let iconname_editor = "edit32"
 let iconname_replay = "refresh32"
 let iconname_remove = "deletefile32"
+let iconname_cleaning = "trashb32"
 
 let image_default = ref (image ~size:20 iconname_default)
 let image_scheduled = ref !image_default
@@ -241,6 +242,7 @@ let image_transf = ref !image_default
 let image_editor = ref !image_default
 let image_replay = ref !image_default
 let image_remove = ref !image_default
+let image_cleaning = ref !image_default
 
 let resize_images size =
   image_default := image ~size iconname_default;
@@ -265,6 +267,7 @@ let resize_images size =
   image_editor := image ~size iconname_editor;
   image_replay := image ~size iconname_replay;
   image_remove := image ~size iconname_remove;
+  image_cleaning := image ~size iconname_cleaning;
   ()
 
 let () =

src/ide/gconfig.mli

@@ -69,6 +69,7 @@ val image_transf : GdkPixbuf.pixbuf ref
 val image_editor : GdkPixbuf.pixbuf ref
 val image_replay : GdkPixbuf.pixbuf ref
 val image_remove : GdkPixbuf.pixbuf ref
+val image_cleaning : GdkPixbuf.pixbuf ref
 
 (* status icons *)
 val image_scheduled : GdkPixbuf.pixbuf ref

src/ide/gmain.ml

@@ -1431,7 +1431,11 @@ let prover_on_selected_goals pr =
 let rec replay_on_goal_or_children g =
   Hashtbl.iter
     (fun _ a -> 
-       if a.Model.proof_obsolete then redo_external_proof g a)
+       if a.Model.proof_obsolete then 
+         match a.Model.proof_state with
+           | Gscheduler.Done { Call_provers.pr_answer = Call_provers.Valid } 
+             -> redo_external_proof g a
+           | _ -> ())
     g.Model.external_proofs;
   Hashtbl.iter
     (fun _ t ->
@@ -2270,10 +2274,8 @@ let () =
 let () =
   let b = GButton.button ~packing:cleaning_box#add ~label:"(clean)" () in
   b#misc#set_tooltip_markup "Not yet implemented";
-(*
-  let i = GMisc.image ~pixbuf:(!image_remove) () in
+  let i = GMisc.image ~pixbuf:(!image_cleaning) () in
   let () = b#set_image i#coerce in
-*)
   let (_ : GtkSignal.id) =
     b#connect#pressed ~callback:not_implemented
   in ()