Commit 373a7bc9 authored by Sylvain Dailler's avatar Sylvain Dailler

Fixes #58

Remove now selects the parent of the removed node when a selected node is
contained in the removed subtree.

Adding a function that check a request is not referring to obsolete
node_id in itp_server.ml. If such a request is found, the error that owuld
have been generated is not sent to the ide.
parent 79da7958
......@@ -2181,7 +2181,24 @@ let treat_notification n =
ignore (new_node id name typ detached)
end
| Remove id ->
(* In the case where id is an ancestor of a selected node, this node will
be erased. So we try to select the parent. *)
let n = get_node_row id in
let is_ancestor =
List.exists
(fun row -> let row_id = get_node_id row#iter in
row_id = id || goals_model#is_ancestor ~iter:n#iter ~descendant:row#iter)
(get_selected_row_references ())
in
if is_ancestor then
(match goals_model#iter_parent n#iter with
| None -> goals_view#selection#unselect_all ()
| Some parent ->
goals_view#selection#unselect_all ();
goals_view#selection#select_iter parent
(* TODO Go to the next unproved goal ?
let parent_id = get_node_id parent in
send_request (Get_first_unproven_node parent_id)*));
ignore (goals_model#remove(n#iter));
Hint.remove node_id_to_gtree id;
Hint.remove node_id_type id;
......
......@@ -1270,6 +1270,23 @@ end
P.notify (Next_Unproven_Node_Id (ni, node_ID_from_any any))
end
(* Check if a request is valid (does not suppose existence of obsolete node_id) *)
let request_is_valid r =
match r with
| Save_req | Reload_req | Unfocus_req | Get_file_contents _ | Save_file_req _
| Interrupt_req | Add_file_req _ | Set_config_param _ | Exit_req -> true
| Get_first_unproven_node ni ->
Hint.mem model_any ni
| Focus_req nid ->
Hint.mem model_any nid
| Remove_subtree nid ->
Hint.mem model_any nid
| Copy_paste (from_id, to_id) ->
Hint.mem model_any from_id && Hint.mem model_any to_id
| Get_task(nid,_,_,_) ->
Hint.mem model_any nid
| Command_req (nid, _) ->
Hint.mem model_any nid
(* ----------------- treat_request -------------------- *)
......@@ -1277,6 +1294,22 @@ end
let treat_request r =
let d = get_server_data () in
let config = d.cont.controller_config in
(* Check that the request does not refer to obsolete node_ids *)
if not (request_is_valid r) then
begin
(* These errors come from the client-server behavior of itp. They cannot
be completely avoided and could be safely ignored.
They are ignored if a debug flag is not added.
*)
if Debug.test_flag Debug.stack_trace then
raise Not_found;
if Debug.test_flag debug then
P.notify (Message (Error (Pp.string_of
(fun fmt r -> Format.fprintf fmt
"The following request refer to obsolete node_ids:\n %a\n"
print_request r) r)))
end
else
try (
match r with
| Save_req -> save_session ()
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment