Adding clean_req. Need testing.

src/ide/why3ide.ml

@@ -525,6 +525,10 @@ let (_ : GMenu.menu_item) =
 let replay_menu_item : GMenu.menu_item =
   file_factory#add_item ~key:GdkKeysyms._R "_Replay all"
 
+let clean_menu_item : GMenu.menu_item =
+  file_factory#add_item ~key:GdkKeysyms._L "C_Lean all"
+    ~callback:(fun _ -> send_request Clean_req)
+
 let (_ : GMenu.menu_item) =
   file_factory#add_item ~key:GdkKeysyms._Q "_Quit"
     ~callback:exit_function_safe

src/session/controller_itp.ml

@@ -689,6 +689,26 @@ let schedule_tr_with_same_arguments
   let name = get_transf_name s tr in
   schedule_transformation c pn name args ~callback ~notification
 
+let clean_session c ~remove ~node_change =
+  let is_valid (pa: proof_attempt_node) : bool =
+    match pa.Session_itp.proof_state with
+    | None -> false
+    | Some pr ->
+      begin
+        match pr.Call_provers.pr_answer with
+        | Call_provers.Valid -> true
+        | _ -> false
+      end
+  in
+  let s = c.controller_session in
+  Session_itp.session_iter_proof_attempt
+    (fun _ pa ->
+      let pnid = pa.parent in
+      Hprover.iter (fun _ paid ->
+        if (not (is_valid (get_proof_attempt_node s paid))) then
+          remove_subtree c ~removed:remove ~node_change (APa paid))
+        (get_proof_attempt_ids s pnid)) s
+
 exception BadCopyPaste
 
 (* Reproduce the transformation made on node on an other one *)

src/session/controller_itp.mli

@@ -210,6 +210,12 @@ val run_strategy_on_goal :
     [schedule_transformation]). [callback] is called on each step of
     execution of the strategy.  *)
 
+val clean_session:
+  controller ->
+  remove:(any -> unit) ->
+  node_change:(any -> bool -> unit) -> unit
+(** Remove proof_attempts that are not valid from the session *)
+
 (* [copy_paste c a b] try to copy subtree originating at node a to node b *)
 val copy_paste:
     notification:(any -> bool -> unit) ->

src/session/itp_communication.ml

@@ -92,6 +92,7 @@ type ide_request =
   | Save_file_req           of string * string
   | Get_first_unproven_node of node_ID
   | Get_Session_Tree_req
+  | Clean_req
   | Save_req
   | Reload_req
   | Replay_req
@@ -103,7 +104,7 @@ let modify_session (r: ide_request) =
   match r with
   | Command_req _ | Prove_req _ | Transform_req _ | Strategy_req _
   | Add_file_req _ | Remove_subtree _ | Copy_paste _ | Copy_detached _
-  | Replay_req -> true
+  | Replay_req | Clean_req -> true
 
   | Open_session_req _ | Set_max_tasks_req _ | Get_file_contents _
   | Get_task _ | Save_file_req _ | Get_first_unproven_node _

src/session/itp_communication.mli

@@ -99,6 +99,7 @@ type ide_request =
   (* Save_file_req (filename, content_of_file). Save the file *)
   | Get_first_unproven_node of node_ID
   | Get_Session_Tree_req
+  | Clean_req
   | Save_req
   | Reload_req
   | Replay_req

src/session/itp_server.ml

@@ -258,6 +258,7 @@ let print_request fmt r =
   | Copy_detached _                 -> fprintf fmt "copy detached"
   | Get_Session_Tree_req            -> fprintf fmt "get session tree"
   | Save_file_req _                 -> fprintf fmt "save file"
+  | Clean_req                       -> fprintf fmt "clean"
   | Save_req                        -> fprintf fmt "save"
   | Reload_req                      -> fprintf fmt "reload"
   | Replay_req                      -> fprintf fmt "replay"
@@ -937,6 +938,20 @@ let () =
                  unproven_goals
     | _ ->  Debug.dprintf debug_strat "[strategy_exec] strategy '%s' not found@." s
 
+
+  (* ----------------- Clean session -------------------- *)
+  let clean_session () =
+    let d = get_server_data () in
+    let node_change x b =
+      let nid = node_ID_from_any x in
+      P.notify (Node_change (nid, Proved b)) in
+    let remove x =
+      let nid = node_ID_from_any x in
+      remove_any_node_ID x;
+      P.notify (Remove nid) in
+    C.clean_session d.cont ~remove ~node_change
+
+
   (* ----------------- Save session --------------------- *)
   let save_session () =
     let d = get_server_data () in
@@ -1012,6 +1027,7 @@ let () =
       end
     | Transform_req (nid, t, args) -> apply_transform nid t args
     | Strategy_req (nid, st)       -> run_strategy_on_task nid st
+    | Clean_req                    -> clean_session ()
     | Save_req                     -> save_session ()
     | Reload_req                   -> reload_session ()
     | Get_Session_Tree_req         -> resend_the_tree ()

src/session/json_util.ml

@@ -125,6 +125,7 @@ let convert_request_constructor (r: ide_request) =
   | Copy_detached _           -> String "Copy_detached"
   | Get_first_unproven_node _ -> String "Get_first_unproven_node"
   | Get_Session_Tree_req      -> String "Get_Session_Tree_req"
+  | Clean_req                 -> String "Clean_req"
   | Save_req                  -> String "Save_req"
   | Reload_req                -> String "Reload_req"
   | Replay_req                -> String "Replay_req"
@@ -185,6 +186,8 @@ let print_request_to_json (r: ide_request): Json_base.value =
            "node_ID", Int id]
   | Get_Session_Tree_req ->
       Obj ["ide_request", cc r]
+  | Clean_req ->
+      Obj ["ide_request", cc r]
   | Save_req ->
       Obj ["ide_request", cc r]
   | Reload_req ->
@@ -318,9 +321,9 @@ exception NotProver
 let parse_prover_from_json (j: Json_base.value) =
   match j with
   | Obj ["prover_name", String pn;
-           "prover_version", String pv;
-           "prover_altern", String pa] ->
-            {Whyconf.prover_name = pn; prover_version = pv; prover_altern = pa}
+         "prover_version", String pv;
+         "prover_altern", String pa] ->
+           {Whyconf.prover_name = pn; prover_version = pv; prover_altern = pa}
   | _ -> raise NotProver
 
 exception NotLimit
@@ -328,9 +331,9 @@ exception NotLimit
 let parse_limit_from_json (j: Json_base.value) =
   match j with
   | Obj ["limit_time", Int t;
-           "limit_mem", Int m;
-           "limit_steps", Int s] ->
-             {limit_time = t; limit_mem = m; limit_steps = s}
+         "limit_mem", Int m;
+         "limit_steps", Int s] ->
+           {limit_time = t; limit_mem = m; limit_steps = s}
   | _ -> raise NotLimit
 
 exception NotRequest of string
@@ -371,6 +374,8 @@ let parse_request (constr: string) l =
     Copy_detached n
   | "Get_Session_Tree_req", [] ->
     Get_Session_Tree_req
+  | "Clean_req" , [] ->
+    Clean_req
   | "Save_req", [] ->
     Save_req
   | "Reload_req", [] ->