Skip to content

GitLab

why3
why3
Commit 1b910c91 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files
Options

Focus first implementation

parent 945ca6d4
Hide whitespace changes
Inline Side-by-side
Showing with 165 additions and 76 deletions
src/ide/why3ide.ml
View file @ 1b910c91
......@@ -478,6 +478,13 @@ let mark_obsolete_item =
create_menu_item tools_factory "Mark obsolete"
"Mark all proof nodes below the current selected nodes as obsolete"
let focus_item =
create_menu_item tools_factory "Focus"
"Focus on proof node"
let unfocus_item =
create_menu_item tools_factory "Unfocus"
"Unfocus"
(* 1.3 "View" menu items *)
......@@ -1315,8 +1322,25 @@ let () =
| [r] ->
let id = get_node_id r#iter in
send_request (Mark_obsolete_req id)
| _ -> print_message "Select only one node to perform this action")
| _ -> print_message "Select only one node to perform this action");
connect_menu_item
focus_item
~callback:(fun () ->
match get_selected_row_references () with
| [r] ->
let id = get_node_id r#iter in
send_request (Focus_req id);
(* TODO not efficient *)
clear_tree_and_table goals_model;
send_request (Get_Session_Tree_req);
| _ -> print_message "Select only one node to perform this action");
connect_menu_item
unfocus_item
~callback:(fun () ->
send_request Unfocus_req;
(* TODO not efficient *)
clear_tree_and_table goals_model;
send_request (Get_Session_Tree_req))
(*************************************)
......
src/session/itp_communication.ml
View file @ 1b910c91
......@@ -100,6 +100,8 @@ type ide_request =
| Set_max_tasks_req of int
| Get_file_contents of string
| Get_task of node_ID
| Focus_req of node_ID
| Unfocus_req
| Remove_subtree of node_ID
| Copy_paste of node_ID * node_ID
| Copy_detached of node_ID
......@@ -125,4 +127,4 @@ let modify_session (r: ide_request) =
| Set_max_tasks_req _ | Get_file_contents _
| Get_task _ | Save_file_req _ | Get_first_unproven_node _
| Get_Session_Tree_req | Save_req | Reload_req | Exit_req
| Interrupt_req -> false
| Interrupt_req | Focus_req _ | Unfocus_req -> false
src/session/itp_communication.mli
View file @ 1b910c91
......@@ -106,6 +106,9 @@ type ide_request =
| Set_max_tasks_req of int
| Get_file_contents of string
| Get_task of node_ID
| Focus_req of node_ID
(* Focus on a node. The server only sends info about descendants of this ID *)
| Unfocus_req
| Remove_subtree of node_ID
| Copy_paste of node_ID * node_ID
| Copy_detached of node_ID
......
src/session/itp_server.ml
View file @ 1b910c91
......@@ -256,6 +256,8 @@ let print_request fmt r =
| Get_file_contents _f -> fprintf fmt "get file contents"
| Get_first_unproven_node _nid -> fprintf fmt "get first unproven node"
| Get_task _nid -> fprintf fmt "get task"
| Focus_req _nid -> fprintf fmt "focus"
| Unfocus_req -> fprintf fmt "unfocus"
| Remove_subtree _nid -> fprintf fmt "remove subtree"
| Copy_paste _ -> fprintf fmt "copy paste"
| Copy_detached _ -> fprintf fmt "copy detached"
......@@ -325,7 +327,7 @@ module type Protocol = sig
val notify : notification -> unit
end
module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
module Make (S:Controller_itp.Scheduler) (Pr:Protocol) = struct
module C = Controller_itp.Make(S)
......@@ -384,6 +386,79 @@ let () =
exit 1
| Some x -> x
(* fresh gives new fresh "names" for node_ID using a counter.
reset resets the counter so that we can regenerate node_IDs as if session
was fresh *)
let reset, fresh =
let count = ref 0 in
(fun () ->
count := 0),
fun () ->
count := !count + 1;
!count
let model_any : any Hint.t = Hint.create 17
let any_from_node_ID (nid:node_ID) : any = Hint.find model_any nid
let pan_to_node_ID : node_ID Hpan.t = Hpan.create 17
let pn_to_node_ID : node_ID Hpn.t = Hpn.create 17
let tn_to_node_ID : node_ID Htn.t = Htn.create 17
let th_to_node_ID : node_ID Ident.Hid.t = Ident.Hid.create 7
let file_to_node_ID : node_ID Hstr.t = Hstr.create 3
let node_ID_from_pan pan = Hpan.find pan_to_node_ID pan
let node_ID_from_pn pn = Hpn.find pn_to_node_ID pn
let node_ID_from_tn tn = Htn.find tn_to_node_ID tn
let node_ID_from_th th = Ident.Hid.find th_to_node_ID (theory_name th)
let node_ID_from_file file = Hstr.find file_to_node_ID (file.file_name)
let node_ID_from_any any =
match any with
| AFile file -> node_ID_from_file file
| ATh th -> node_ID_from_th th
| ATn tn -> node_ID_from_tn tn
| APn pn -> node_ID_from_pn pn
| APa pan -> node_ID_from_pan pan
let remove_any_node_ID any =
match any with
| AFile file ->
let nid = Hstr.find file_to_node_ID file.file_name in
Hint.remove model_any nid;
Hstr.remove file_to_node_ID file.file_name
| ATh th ->
let nid = Ident.Hid.find th_to_node_ID (theory_name th) in
Hint.remove model_any nid;
Ident.Hid.remove th_to_node_ID (theory_name th)
| ATn tn ->
let nid = Htn.find tn_to_node_ID tn in
Hint.remove model_any nid;
Htn.remove tn_to_node_ID tn
| APn pn ->
let nid = Hpn.find pn_to_node_ID pn in
Hint.remove model_any nid;
Hpn.remove pn_to_node_ID pn
| APa pa ->
let nid = Hpan.find pan_to_node_ID pa in
Hint.remove model_any nid;
Hpan.remove pan_to_node_ID pa
let get_prover p =
let d = get_server_data () in
match return_prover p d.cont.controller_config with
| None -> raise (Bad_prover_name p)
| Some c -> c
let add_node_to_table node new_id =
match node with
| AFile file -> Hstr.add file_to_node_ID file.file_name new_id
| ATh th -> Ident.Hid.add th_to_node_ID (theory_name th) new_id
| ATn tn -> Htn.add tn_to_node_ID tn new_id
| APn pn -> Hpn.add pn_to_node_ID pn new_id
| APa pan -> Hpan.add pan_to_node_ID pan new_id
(*******************************)
(* Compute color for locations *)
(*******************************)
......@@ -450,6 +525,44 @@ let get_locations t =
get_locations l t;
!l
let get_modified_node n =
match n with
| New_node (nid, _, _, _, _) -> Some nid
| Node_change (nid, _) -> Some nid
| Remove nid -> Some nid
| Next_Unproven_Node_Id (_, nid) -> Some nid
| Initialized _ -> None
| Saved -> None
| Message _ -> None
| Dead _ -> None
| Task (nid, _, _) -> Some nid
| File_contents _ -> None
(* Focus on a node *)
let focused_node = ref None
(* TODO *)
module P = struct
let get_requests = Pr.get_requests
let notify n =
let d = get_server_data() in
let s = d.cont.controller_session in
match !focused_node with
| None -> Pr.notify n
| Some f_node ->
let updated_node = get_modified_node n in
match updated_node with
| None -> Pr.notify n
| Some nid when
let any = any_from_node_ID nid in
Session_itp.is_below s any f_node ->
Pr.notify n
| _ -> ()
end
(*********************)
(* File input/output *)
(*********************)
......@@ -602,78 +715,6 @@ let get_locations t =
{name; proved}
*)
(* fresh gives new fresh "names" for node_ID using a counter.
reset resets the counter so that we can regenerate node_IDs as if session
was fresh *)
let reset, fresh =
let count = ref 0 in
(fun () ->
count := 0),
fun () ->
count := !count + 1;
!count
let model_any : any Hint.t = Hint.create 17
let any_from_node_ID (nid:node_ID) : any = Hint.find model_any nid
let pan_to_node_ID : node_ID Hpan.t = Hpan.create 17
let pn_to_node_ID : node_ID Hpn.t = Hpn.create 17
let tn_to_node_ID : node_ID Htn.t = Htn.create 17
let th_to_node_ID : node_ID Ident.Hid.t = Ident.Hid.create 7
let file_to_node_ID : node_ID Hstr.t = Hstr.create 3
let node_ID_from_pan pan = Hpan.find pan_to_node_ID pan
let node_ID_from_pn pn = Hpn.find pn_to_node_ID pn
let node_ID_from_tn tn = Htn.find tn_to_node_ID tn
let node_ID_from_th th = Ident.Hid.find th_to_node_ID (theory_name th)
let node_ID_from_file file = Hstr.find file_to_node_ID (file.file_name)
let node_ID_from_any any =
match any with
| AFile file -> node_ID_from_file file
| ATh th -> node_ID_from_th th
| ATn tn -> node_ID_from_tn tn
| APn pn -> node_ID_from_pn pn
| APa pan -> node_ID_from_pan pan
let remove_any_node_ID any =
match any with
| AFile file ->
let nid = Hstr.find file_to_node_ID file.file_name in
Hint.remove model_any nid;
Hstr.remove file_to_node_ID file.file_name
| ATh th ->
let nid = Ident.Hid.find th_to_node_ID (theory_name th) in
Hint.remove model_any nid;
Ident.Hid.remove th_to_node_ID (theory_name th)
| ATn tn ->
let nid = Htn.find tn_to_node_ID tn in
Hint.remove model_any nid;
Htn.remove tn_to_node_ID tn
| APn pn ->
let nid = Hpn.find pn_to_node_ID pn in
Hint.remove model_any nid;
Hpn.remove pn_to_node_ID pn
| APa pa ->
let nid = Hpan.find pan_to_node_ID pa in
Hint.remove model_any nid;
Hpan.remove pan_to_node_ID pa
let get_prover p =
let d = get_server_data () in
match return_prover p d.cont.controller_config with
| None -> raise (Bad_prover_name p)
| Some c -> c
let add_node_to_table node new_id =
match node with
| AFile file -> Hstr.add file_to_node_ID file.file_name new_id
| ATh th -> Ident.Hid.add th_to_node_ID (theory_name th) new_id
| ATn tn -> Htn.add tn_to_node_ID tn new_id
| APn pn -> Hpn.add pn_to_node_ID pn new_id
| APa pan -> Hpan.add pan_to_node_ID pan new_id
(* Create a new node in the_tree, update the tables and send a
notification about it *)
let new_node ~parent node : node_ID =
......@@ -1117,6 +1158,11 @@ let get_locations t =
| Get_Session_Tree_req -> resend_the_tree ()
| Get_first_unproven_node ni ->
notify_first_unproven_node d ni
| Focus_req nid ->
let any = any_from_node_ID nid in
focused_node := Some any
| Unfocus_req ->
focused_node := None
| Remove_subtree nid ->
let n = any_from_node_ID nid in
begin
......
src/session/json_util.ml
View file @ 1b910c91
......@@ -129,6 +129,8 @@ let convert_request_constructor (r: ide_request) =
| Save_file_req _ -> String "Save_file_req"
| Set_max_tasks_req _ -> String "Set_max_tasks_req"
| Get_file_contents _ -> String "Get_file_contents"
| Focus_req _ -> String "Focus_req"
| Unfocus_req -> String "Unfocus_req"
| Get_task _ -> String "Get_task"
| Remove_subtree _ -> String "Remove_subtree"
| Copy_paste _ -> String "Copy_paste"
......@@ -202,6 +204,11 @@ let print_request_to_json (r: ide_request): Json_base.json =
| Get_first_unproven_node id ->
convert_record ["ide_request", cc r;
"node_ID", Int id]
| Focus_req id ->
convert_record ["ide_request", cc r;
"node_ID", Int id]
| Unfocus_req ->
convert_record ["ide_request", cc r]
| Get_Session_Tree_req ->
convert_record ["ide_request", cc r]
| Mark_obsolete_req n ->
......@@ -452,6 +459,13 @@ let parse_request (constr: string) j =
let f = get_string (get_field j "file") in
Open_session_req f
*)
| "Focus_req" ->
let nid = get_int (get_field j "node_ID") in
Focus_req nid
| "Unfocus_req" ->
Unfocus_req
| "Add_file_req" ->
let f = get_string (get_field j "file") in
Add_file_req f
......
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