diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml index cd478bb7db6cec334007f0da650173f1c69bd5c9..208a63ab191ad7221ab4f89a3ddf68333ca23a00 100644 --- a/src/ide/why3ide.ml +++ b/src/ide/why3ide.ml @@ -375,7 +375,7 @@ let (_ : GMenu.menu_item) = (* TODO key stroked to be decided *) let reload_menu_item : GMenu.menu_item = - file_factory#add_item ~key:GdkKeysyms._E "_Reload session" + file_factory#add_item ~key:GdkKeysyms._E "r_Eload session" ~callback:(fun () -> (* Clearing the tree *) clear_tree_and_table goals_model; @@ -428,6 +428,17 @@ let message_zone = GText.view ~editable:false ~cursor_visible:false ~packing:sv#add () +(**** Message-zone printing functions *****) + +(* Function used to print stuff on the message_zone *) +let print_message s = + message_zone#buffer#set_text s + +let add_to_msg_zone s = + let s = message_zone#buffer#get_text () ^ "\n" ^ s in + message_zone#buffer#set_text s; + message_zone#scroll_to_mark `INSERT + (**** Monitor *****) let fan n = @@ -748,19 +759,66 @@ let (_ : GtkSignal.id) = | [r] -> on_selected_row r | _ -> ()) +let remove_item: GMenu.menu_item = + file_factory#add_item "Remove" + ~callback:(fun () -> + match get_selected_row_references () with + | [r] -> let id = get_node_id r#iter in send_request (Remove_subtree id) + | _ -> print_message "Select only one node to perform this action") + +(*********************************) +(* add a new file in the project *) +(*********************************) + +let filter_all_files () = + let f = GFile.filter ~name:"All" () in + f#add_pattern "*" ; + f + +let filter_why_files () = + GFile.filter + ~name:"Why3 source files" + ~patterns:[ "*.why"; "*.mlw"] () + +let select_file ~request = + let d = GWindow.file_chooser_dialog ~action:`OPEN + ~title:"Why3: Add file in project" + () + in + d#add_button_stock `CANCEL `CANCEL ; + d#add_select_button_stock `OPEN `OPEN ; + d#add_filter (filter_why_files ()) ; + d#add_filter (filter_all_files ()) ; + begin match d#run () with + | `OPEN -> + begin + match d#filename with + | None -> () + | Some f -> request f + end + | `DELETE_EVENT | `CANCEL -> () + end ; + d#destroy () + +let open_item: GMenu.menu_item = + file_factory#add_item ~key:GdkKeysyms._A "_Add file" + ~callback:(fun () -> + select_file ~request:(fun f -> send_request (Add_file_req f))) + +let open_session: GMenu.menu_item = + file_factory#add_item ~key:GdkKeysyms._O "Open session" + ~callback:(fun () -> + select_file ~request:(fun f -> + (* Clearing the ide tree *) + clear_tree_and_table goals_model; + (* Adding the root again *) + create_root (); + send_request (Open_session_req f))) + (*************************) (* Notification Handling *) (*************************) -(* Function used to print stuff on the message_zone *) -let print_message s = - message_zone#buffer#set_text s - -let add_to_msg_zone s = - let s = message_zone#buffer#get_text () ^ "\n" ^ s in - message_zone#buffer#set_text s; - message_zone#scroll_to_mark `INSERT - let treat_message_notification msg = match msg with (* TODO: do something ! *) | Proof_error (_id, s) -> print_message s @@ -773,7 +831,6 @@ let treat_message_notification msg = match msg with | Information s -> print_message s | Task_Monitor (t, s, r) -> update_monitor t s r | Open_File_Error s -> print_message s - (* TODO do not print this particular error *) | Error s -> if Debug.test_flag debug then print_message s @@ -808,8 +865,15 @@ let treat_notification n = match n with (* TODO for easier testing of IDE *) if typ = NGoal then goals_view#selection#select_iter row_ref#iter); end - | Remove _id -> (* TODO *) - print_message "got a Remove notification not yet supported\n" + | Remove id -> + let n = get_node_row id in + begin + ignore (goals_model#remove(n#iter)); + Hint.remove node_id_to_gtree id; + Hint.remove node_id_type id; + Hint.remove node_id_proved id; + Hint.remove node_id_pa id + end | Initialized g_info -> (* TODO: treat other *) init_completion g_info.provers g_info.transformations g_info.commands; diff --git a/src/printer/why3printer.mli b/src/printer/why3printer.mli index 500a5ad6b7c55394a446da5093235cceed11adde..2081a47c8062a908afa63c40293a6856fd664c8f 100644 --- a/src/printer/why3printer.mli +++ b/src/printer/why3printer.mli @@ -20,8 +20,6 @@ *) -open Ident - val print_ls : Task.name_tables -> Format.formatter -> Term.lsymbol -> unit val print_tv : Task.name_tables -> Format.formatter -> Ty.tvsymbol -> unit val print_ts : Task.name_tables -> Format.formatter -> Ty.tysymbol -> unit diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml index 418326ba25bca45f7e513746d4dc0e1b0b914f51..682d5ab3ae241aaf929fd59c503baa80f1a4c381 100644 --- a/src/session/itp_server.ml +++ b/src/session/itp_server.ml @@ -371,6 +371,7 @@ type ide_request = | Add_file_req of string | Set_max_tasks_req of int | Get_task of node_ID + | Remove_subtree of node_ID | Get_Session_Tree_req | Save_req | Reload_req @@ -388,6 +389,7 @@ let print_request fmt r = | Add_file_req f -> fprintf fmt "open file %s" f | Set_max_tasks_req i -> fprintf fmt "set max tasks %i" i | Get_task _nid -> fprintf fmt "get task" + | Remove_subtree _nid -> fprintf fmt "remove subtree" | Get_Session_Tree_req -> fprintf fmt "get session tree" | Save_req -> fprintf fmt "save" | Reload_req -> fprintf fmt "reload" @@ -411,7 +413,7 @@ let print_msg fmt m = let print_notify fmt n = match n with | Node_change (_ni, _nf) -> fprintf fmt "node change" - | New_node (ni, _pni, _nt, _nf) -> fprintf fmt "new node %d" ni + | New_node (ni, _pni, _nt, _nf) -> fprintf fmt "new node %d" ni | Remove _ni -> fprintf fmt "remove" | Initialized _gi -> fprintf fmt "initialized" | Saved -> fprintf fmt "saved" @@ -434,7 +436,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct type server_data = { config : Whyconf.config; task_driver : Driver.driver; - provers : Whyconf.config_prover Whyconf.Mprover.t; + sd_provers : Whyconf.config_prover Whyconf.Mprover.t; cont : Controller_itp.controller; } @@ -482,7 +484,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct server_data := Some { config = config; task_driver = task_driver; - provers = provers; + sd_provers = provers; cont = c } (* ------------ init controller ------------ *) @@ -944,6 +946,16 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct | Save_req -> save_session () | Reload_req -> reload_session (); | Get_Session_Tree_req -> resend_the_tree () + | Remove_subtree nid -> + let n = any_from_node_ID nid in + begin + try + Session_itp.remove_subtree d.cont.controller_session n ~notification:(fun x -> + let nid = node_ID_from_any x in + P.notify (Remove nid)) + with RemoveError -> (* TODO send an error instead of information *) + P.notify (Message (Information "Cannot remove a proof node or theory")) + end | Get_task nid -> send_task nid | Replay_req -> replay_session (); resend_the_tree () | Command_req (nid, cmd) -> diff --git a/src/session/itp_server.mli b/src/session/itp_server.mli index 92f0367a838a0f4e9d0bd89b68812e30580b8183..718698edc3736a16f196b4e89bb48cd6fcde0d6a 100644 --- a/src/session/itp_server.mli +++ b/src/session/itp_server.mli @@ -85,6 +85,7 @@ type ide_request = | Add_file_req of string | Set_max_tasks_req of int | Get_task of node_ID + | Remove_subtree of node_ID | Get_Session_Tree_req | Save_req | Reload_req diff --git a/src/session/server_utils.ml b/src/session/server_utils.ml index a2b2a43d4eaf940dc72279cda3ec5d616bc4baa1..f05e2d6bbfaf739dbb12303247527eb35b4c09ba 100644 --- a/src/session/server_utils.ml +++ b/src/session/server_utils.ml @@ -25,7 +25,7 @@ let cont_from_session_dir cont dir = eprintf "using shapes: %a@." pp_print_bool use_shapes; (* create the controller *) Controller_itp.init_controller ses cont; - (* update the session *) + (* update the session *) Controller_itp.reload_files cont ~use_shapes (* If we have a file we chop it and return new session based on the directory *) diff --git a/src/session/session_itp.ml b/src/session/session_itp.ml index a3bfc44ba578e9b44dfb551146ef55da00aaf379..12b76f33b02afc2ffc8856edfe0f4a5ac64a005a 100644 --- a/src/session/session_itp.ml +++ b/src/session/session_itp.ml @@ -70,22 +70,8 @@ type any = | APn of proofNodeID | APa of proofAttemptID -module Proofnodeid = struct - type t = proofNodeID - let _compare (x : proofNodeID) y = Pervasives.compare x y - let equal (x : proofNodeID) y = x = y - let hash (x : proofNodeID) = x -end - -module Transid = struct - type t = transID - let _compare (x : transID) y = Pervasives.compare x y - let equal (x : transID) y = x = y - let hash (x : transID) = x -end - -module Hpn = Exthtbl.Make(Proofnodeid) -module Htn = Exthtbl.Make(Transid) +module Hpn = Hint +module Htn = Hint module Hpan = Hint type session = { @@ -185,6 +171,7 @@ let get_trans (s : session) (n : int) = let _ = Hint.find s.trans_table n in n *) +(* Generation of new IDs *) let gen_transID (s : session) = let id = s.next_transID in s.next_transID <- id + 1; @@ -200,6 +187,8 @@ let gen_proofAttemptID (s : session) = s.next_proofAttemptID <- id + 1; id +(* Get elements of the session tree *) + exception BadID let get_proof_attempt_node (s : session) (id : proofAttemptID) = @@ -261,6 +250,98 @@ let get_proof_parent (s : session) (id : proofNodeID) = let get_trans_parent (s : session) (id : transID) = (get_transfNode s id).transf_parent + +(* Remove elements of the session tree *) + +let remove_transformation (s : session) (id : transID) = + let nt = get_transfNode s id in + Hint.remove s.trans_table id; + let pn = get_proofNode s nt.transf_parent in + let trans_up = List.filter (fun tid -> tid != id) pn.proofn_transformations in + pn.proofn_transformations <- trans_up + +let remove_proof_attempt (s : session) (id : proofNodeID) + (prover : Whyconf.prover) = + let pn = get_proofNode s id in + let pa = Hprover.find pn.proofn_attempts prover in + Hprover.remove pn.proofn_attempts prover; + Hint.remove s.proofAttempt_table pa + +let remove_proof_attempt_pa s (id: proofAttemptID) = + let pa = get_proof_attempt_node s id in + let pn = pa.parent in + let prover = pa.prover in + remove_proof_attempt s pn prover + +(* Iterations functions on the session tree *) + +let rec fold_all_any_of_transn s f acc trid = + let tr = get_transfNode s trid in + let acc = + List.fold_left + (fold_all_any_of_proofn s f) + acc tr.transf_subtasks + in + f acc (ATn trid) + +and fold_all_any_of_proofn s f acc pnid = + let pn = get_proofNode s pnid in + let acc = + List.fold_left + (fun acc trid -> + fold_all_any_of_transn s f acc trid) + acc pn.proofn_transformations + in + let acc = + Hprover.fold + (fun _p paid acc -> + f acc (APa paid)) + pn.proofn_attempts acc + in + f acc (APn pnid) + +let fold_all_any_of_theory s f acc th = + let acc = List.fold_left (fold_all_any_of_proofn s f) acc th.theory_goals in + f acc (ATh th) + +let fold_all_any_of_file s f acc file = + let acc = List.fold_left (fold_all_any_of_theory s f) acc file.file_theories in + f acc (AFile file) + +let fold_all_any s f acc any = + match any with + | AFile file -> fold_all_any_of_file s f acc file + | ATh th -> fold_all_any_of_theory s f acc th + | APn pn -> fold_all_any_of_proofn s f acc pn + | ATn tn -> fold_all_any_of_transn s f acc tn + | APa _ -> f acc any + +exception RemoveError + +let remove_subtree s (n: any) ~notification : unit = + + let remove s (n: any) = + (* These removal functions should not be used for direct removal: subtrees + must be removed first. *) + let remove_file s (f: file) = + Hstr.remove s.session_files f.file_name in + let remove_proof_node s pnid = + Hint.remove s.proofNode_table pnid in + let remove_theory _s (_th: theory) = + (* Not in any table *) + () in + match n with + | ATn tn -> remove_transformation s tn + | APa pa -> remove_proof_attempt_pa s pa + | AFile f -> remove_file s f + | APn pn -> remove_proof_node s pn + | ATh th -> remove_theory s th + in + match n with + | APn _pn -> raise RemoveError + | ATh _th -> raise RemoveError + | _ -> ignore (fold_all_any s (fun acc x -> remove s x; notification x; acc) [] n) + let rec fold_all_sub_goals_of_proofn s f acc pnid = let pn = get_proofNode s pnid in let acc = @@ -384,10 +465,6 @@ let graft_proof_attempt (s : session) (id : proofNodeID) (pr : Whyconf.prover) Call_provers.limit_steps = -1; } in add_proof_attempt s pr limit None false None id -let remove_proof_attempt (s : session) (id : proofNodeID) - (prover : Whyconf.prover) = - let pn = get_proofNode s id in - Hprover.remove pn.proofn_attempts prover (* [mk_proof_node s n t p id] register in the session [s] a proof node of proofNodeID [id] of parent [p] of task [t] *) @@ -455,12 +532,6 @@ let graft_transf (s : session) (id : proofNodeID) (name : string) mk_transf_node s id tid name args sub_tasks; tid -let remove_transformation (s : session) (id : transID) = - let nt = get_transfNode s id in - Hint.remove s.trans_table id; - let pn = get_proofNode s nt.transf_parent in - let trans_up = List.filter (fun tid -> tid != id) pn.proofn_transformations in - pn.proofn_transformations <- trans_up let update_proof_attempt s id pr st = let n = get_proofNode s id in @@ -1114,8 +1185,6 @@ let make_theory_section ~use_shapes ?merge (s:session) parent_name (th:Theory.th let add_file_section ~use_shapes (s:session) (fn:string) (theories:Theory.theory list) format : unit = let fn = Sysutil.relativize_filename s.session_dir fn in - Format.eprintf "TODO %s\n" fn; - Hstr.iter (fun x _i -> Format.eprintf "TOD %s\n" x) s.session_files; if Hstr.mem s.session_files fn then Debug.dprintf debug "[session] file %s already in database@." fn else diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli index af060cda5a33422da0255e6740882fdec980b5bf..f93c95a409d54cb233f4f15d3472250384cb4f4e 100644 --- a/src/session/session_itp.mli +++ b/src/session/session_itp.mli @@ -156,3 +156,11 @@ val load_session : string -> session * bool raises [ShapesFileError msg] if the database extra file for shapes cannot be read. *) + +exception RemoveError + +val remove_subtree: session -> any -> notification:(any -> unit) -> unit +(** [remove_subtree s a notification] remove the subtree originating from a in + session s then call the notification function (used to notify the ide. + + If called on a theory or proof node, raise RemoveError *)