Commit 30f8256a authored by Sylvain Dailler's avatar Sylvain Dailler

IDE: fix #148 use select_iter instead of selection#select_iter

select_iter changes the cursor used by the goals_view for changing nodes
with keyboard arrow keys. selection#select_iter should be avoided alone.
parent 917cd4c9
...@@ -1218,6 +1218,16 @@ let get_selected_row_references () = ...@@ -1218,6 +1218,16 @@ let get_selected_row_references () =
(**********************) (**********************)
(* Contextual actions *) (* Contextual actions *)
(**********************) (**********************)
(* goals_view#selection#select_iter only changes the selection for the selection
tree, it should also change the cursor of the goal_view. The reason is that
the cursor is used for arrow keys moves (not the selected row). *)
let select_iter iter =
goals_view#selection#select_iter iter;
let path = goals_model#get_path iter in
goals_view#set_cursor path view_name_column
let expand_row () = let expand_row () =
let rows = get_selected_row_references () in let rows = get_selected_row_references () in
match rows with match rows with
...@@ -1243,7 +1253,7 @@ let move_current_row_selection_to_parent () = ...@@ -1243,7 +1253,7 @@ let move_current_row_selection_to_parent () =
match goals_model#iter_parent row#iter with match goals_model#iter_parent row#iter with
| None -> () | None -> ()
| Some iter -> | Some iter ->
goals_view#selection#select_iter iter select_iter iter
end end
| _ -> () | _ -> ()
...@@ -1258,7 +1268,7 @@ let move_current_row_selection_to_first_child () = ...@@ -1258,7 +1268,7 @@ let move_current_row_selection_to_first_child () =
begin begin
goals_view#selection#unselect_all (); goals_view#selection#unselect_all ();
let iter = goals_model#iter_children ?nth:(Some 0) (Some row#iter) in let iter = goals_model#iter_children ?nth:(Some 0) (Some row#iter) in
goals_view#selection#select_iter iter select_iter iter
end end
| _ -> () | _ -> ()
...@@ -2350,7 +2360,7 @@ let treat_notification n = ...@@ -2350,7 +2360,7 @@ let treat_notification n =
proof, it is better to only have the new goal selected *) proof, it is better to only have the new goal selected *)
goals_view#selection#unselect_all (); goals_view#selection#unselect_all ();
let iter = (get_node_row next_unproved_id)#iter in let iter = (get_node_row next_unproved_id)#iter in
goals_view#selection#select_iter iter select_iter iter
end end
| New_node (id, parent_id, typ, name, detached) -> | New_node (id, parent_id, typ, name, detached) ->
begin begin
...@@ -2382,7 +2392,7 @@ let treat_notification n = ...@@ -2382,7 +2392,7 @@ let treat_notification n =
| None -> goals_view#selection#unselect_all () | None -> goals_view#selection#unselect_all ()
| Some parent -> | Some parent ->
goals_view#selection#unselect_all (); goals_view#selection#unselect_all ();
goals_view#selection#select_iter parent select_iter parent
(* TODO Go to the next unproved goal ? (* TODO Go to the next unproved goal ?
let parent_id = get_node_id parent in let parent_id = get_node_id parent in
send_request (Get_first_unproven_node parent_id)*)); send_request (Get_first_unproven_node parent_id)*));
...@@ -2397,7 +2407,7 @@ let treat_notification n = ...@@ -2397,7 +2407,7 @@ let treat_notification n =
display_warnings (); display_warnings ();
init_completion g_info.provers g_info.transformations g_info.strategies g_info.commands; init_completion g_info.provers g_info.transformations g_info.strategies g_info.commands;
complete_context_menu (); complete_context_menu ();
Opt.iter goals_view#selection#select_iter goals_model#get_iter_first Opt.iter select_iter goals_model#get_iter_first
| Saved -> | Saved ->
session_needs_saving := false; session_needs_saving := false;
print_message ~kind:1 ~notif_kind:"Saved action info" print_message ~kind:1 ~notif_kind:"Saved action info"
......
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