Can now remove detached nodes.

src/session/controller_itp.ml

@@ -408,23 +408,29 @@ let add_file c ?format fname =
 let remove_subtree c (n: any) ~removed ~node_change =
   let removed = (fun x -> removed x; remove_any_proof_state c x) in
   let parent = get_any_parent c.controller_session n in
-  match n with
-  | ATn _ | APa _ ->
-    Session_itp.remove_subtree c.controller_session n ~notification:removed;
-    (match parent with
-      | Some (APn parent) ->
-        (* If proof_state of the parent is actually changed update the branch
-           otherwise do nothing *)
-        let tr_list = get_transformations c.controller_session parent in
-        let pa_list = get_proof_attempts c.controller_session parent in
-        let proved = List.exists (tn_proved c) tr_list in
-        let proved = List.exists reload_pa_proof_state pa_list || proved in
-        if proved then
-          ()
-        else
-          update_proof_node node_change c parent false
-    | _ -> assert false)
-  | _ -> ()
+  (* Note that this line can raise RemoveError when called on inappropriate
+     node (attached theory / goals) *)
+  Session_itp.remove_subtree c.controller_session n ~notification:removed;
+  (match parent with
+  | Some (APn parent) ->
+      (* If proof_state of the parent is actually changed update the branch
+         otherwise do nothing *)
+      let tr_list = get_transformations c.controller_session parent in
+      let pa_list = get_proof_attempts c.controller_session parent in
+      let proved = List.exists (tn_proved c) tr_list in
+      let proved = List.exists reload_pa_proof_state pa_list || proved in
+      if proved then
+        ()
+      else
+        update_proof_node node_change c parent false
+  | Some _ ->
+      (* This case corresponds to removal of detached node. We don't need to
+         update the proof_state *)
+      ()
+  | None ->
+      (* Cannot remove root. Note that this should already have failed in call
+         to Session_itp.remove_subtree *)
+      raise RemoveError)
 
 module type Scheduler = sig
   val timeout: ms:int -> (unit -> bool) -> unit

src/session/itp_server.ml

@@ -1015,7 +1015,7 @@ let () =
                         remove_any_node_ID x;
                         P.notify (Remove nid))
         with RemoveError -> (* TODO send an error instead of information *)
-          P.notify (Message (Information "Cannot remove a proof node or theory"))
+          P.notify (Message (Information "Cannot remove attached proof nodes or theories"))
         end
     | Copy_paste (from_id, to_id)    ->
         let from_any = any_from_node_ID from_id in

src/session/session_itp.ml

@@ -369,10 +369,10 @@ let remove_subtree s (n: any) ~notification : unit =
     | ATh th -> remove_theory s th
   in
   match n with
-  | APn _pn -> raise RemoveError
-  | ATh _th -> raise RemoveError
+  | APn _pn when not (is_detached s n) -> raise RemoveError
+  | ATh _th when not (is_detached s n) -> raise RemoveError
   | _ ->
-    ignore (fold_all_any s (fun acc x -> remove s x; notification x; acc) [] n)
+    fold_all_any s (fun _ x -> remove s x; notification x) () n
 
 let rec fold_all_sub_goals_of_proofn s f acc pnid =
   let pn = get_proofNode s pnid in
@@ -568,7 +568,7 @@ let copy_proof_node_as_detached (s: session) (pn_id: proofNodeID) =
   let new_goal = Ident.id_register (Ident.id_clone pn.proofn_name) in
   let checksum = pn.proofn_checksum in
   let shape = pn.proofn_shape in
-  let (_: unit) = mk_proof_node_no_task s new_goal parent new_pn_id checksum shape in
+  let _: unit = mk_proof_node_no_task s new_goal parent new_pn_id checksum shape in
   graft_detached_proof_on_parent s new_pn_id parent;
   new_pn_id