Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 6de885b6 authored by Sylvain Dailler's avatar Sylvain Dailler

Add remove. Add open session in ide. Add add_file in ide.

parent 7b17e4bf
......@@ -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;
......
......@@ -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
......
......@@ -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) ->
......
......@@ -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
......
......@@ -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 *)
......
......@@ -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
......
......@@ -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 *)
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