avoid bomb in case of uninstalled prover

src/ide/why3ide.ml

@@ -999,8 +999,7 @@ let image_of_pa_status ~obsolete pa =
   | Controller_itp.Scheduled -> !image_scheduled
   | Controller_itp.Running -> !image_running
   | Controller_itp.InternalFailure _e -> !image_failure
-  | Controller_itp.Uninstalled _p -> !image_failure (* TODO !image_uninstalled *)
-(*  | None -> !image_undone*)
+  | Controller_itp.Uninstalled _p -> !image_undone (* TODO !image_uninstalled *)
   | Controller_itp.Done r ->
     let pr_answer = r.Call_provers.pr_answer in
     begin

src/session/controller_itp.ml

@@ -863,7 +863,10 @@ let replay ?(obsolete_only=true) ?(use_steps=false)
       begin
         let parid = pa.parent in
         let pr = pa.prover in
-        (* If use_steps, we give only steps as a limit *)
+        (* TODO: if pr is not installed, lookup for a replacement policy
+         OR: delegate this work to the replay_proof_attempt function *)
+        (* If use_steps, we give only steps as a limit
+         TODO: steps should not be used if prover was replaced above *)
         let limit =
           if use_steps then
             Call_provers.{empty_limit with limit_steps = pa.limit.limit_steps}

src/session/itp_server.ml

@@ -903,7 +903,7 @@ let get_locations t =
           let parent = node_ID_from_pn parent_id in
           ignore (new_node ~parent (APa panid))
       end
-    | _  -> () (* TODO ? *)
+    | _  -> () (* TODO ? status like Uninstalled should not generate a Notification *)
     end;
     let limit = (get_proof_attempt_node cont.controller_session panid).limit in
     let new_status = Proof_status_change (pa_status, false, limit) in