Commit 28ab37cf authored by Sylvain Dailler's avatar Sylvain Dailler Committed by MARCHE Claude

Add move source file in the IDE

parent 1f3e77e2
......@@ -372,6 +372,9 @@ let record_warning ?loc msg =
(Pp.print_option Loc.report_position) loc msg;
Queue.push (loc,msg) warnings
(* Keep the current session dir in memory *)
let session_dir = ref ""
let () =
Warning.set_hook record_warning;
let dir =
......@@ -381,6 +384,7 @@ let () =
Format.eprintf "Error: %s@." s;
Whyconf.Args.exit_with_usage spec usage_str
in
session_dir := dir;
Server.init_server gconfig.config env dir;
Queue.iter (fun f -> send_request (Add_file_req f)) files;
send_request Get_global_infos;
......@@ -2138,6 +2142,10 @@ let paste_item =
~modi:[`CONTROL] ~key:GdkKeysyms._V
~tooltip:"Paste the copied node below the current node"
let move_source_file_item =
tools_factory#add_item "Move source file"
~tooltip:"Move source file"
(* complete the contextual menu (but only after provers and strategies, hence the function) *)
let complete_context_menu () =
......@@ -2233,6 +2241,60 @@ let () =
connect_menu_item copy_item ~callback:copy;
connect_menu_item paste_item ~callback:paste
(********************)
(* Move source file *)
(********************)
let move_source_file () =
let note_page = notebook#current_page in
let from_file =
let module M = struct exception Found of string end in
try
Hstr.iter (fun fname (page_num, _, _, _) ->
if page_num = note_page then
raise (M.Found fname)) source_view_table;
None
with M.Found fname -> Some fname
in
match from_file with
| None -> print_message ~kind:1 ~notif_kind:"Move file" "select a source file tab to move."
| Some from_file ->
let to_file =
let d = GWindow.file_chooser_dialog ~action:`SAVE
~title:"Select a new file to move to"
()
in
d#add_button_stock `CANCEL `CANCEL ;
d#add_select_button_stock `SAVE `SAVE ;
d#add_filter (filter_why_files ()) ;
d#add_filter (filter_all_files ()) ;
let module M = struct exception Found of string end in
try
begin match d#run () with
| `SAVE ->
begin
match d#filename with
| None -> ()
| Some f -> raise (M.Found f)
end
| `DELETE_EVENT | `CANCEL -> ()
end ;
d#destroy ();
None
with M.Found f -> d#destroy (); Some f
in
match to_file with
| None -> print_message ~kind:1 ~notif_kind:"Move file" "Error when selecting file to move to."
| Some to_file ->
let to_file = Sysutil.relativize_filename !session_dir to_file in
notebook#remove_page note_page;
Hstr.remove source_view_table from_file;
clear_tree_and_table goals_model;
send_request (Move_source_req (from_file, to_file))
let () =
connect_menu_item move_source_file_item ~callback:move_source_file
(**********************************)
(* Notification handling (part 2) *)
(**********************************)
......
......@@ -117,6 +117,7 @@ type ide_request =
| Copy_paste of node_ID * node_ID
| Save_file_req of string * string
| Get_first_unproven_node of node_ID
| Move_source_req of string * string
| Unfocus_req
| Save_req
| Reload_req
......@@ -144,6 +145,7 @@ let print_request fmt r =
| Remove_subtree _nid -> fprintf fmt "remove subtree"
| Copy_paste _ -> fprintf fmt "copy paste"
| Save_file_req _ -> fprintf fmt "save file"
| Move_source_req _ -> fprintf fmt "move source file"
| Unfocus_req -> fprintf fmt "unfocus"
| Save_req -> fprintf fmt "save"
| Reload_req -> fprintf fmt "reload"
......
......@@ -135,6 +135,9 @@ type ide_request =
| Save_file_req of string * string
(** [Save_file_req(filename, content_of_file)] saves the file *)
| Get_first_unproven_node of node_ID
| Move_source_req of string * string
(** [Move_source_req(from_file, to_file)] request to move source [from_file]
to location [to_file]. file path are given relative to session directory. *)
| Unfocus_req
| Save_req
| Reload_req
......
......@@ -1364,13 +1364,52 @@ end
P.notify (Next_Unproven_Node_Id (ni, node_ID_from_any any))
end
(* [move_source_file d from_file to_file]: Move a source file from the IDE
both in the session and on the filesystem.
[from_file] and [to_file] are relative to the session directory.
*)
let move_source_file d from_file to_file =
let s = d.cont.controller_session in
let session_dir = Session_itp.get_dir s in
let abs_from_file = Filename.concat session_dir from_file in
let abs_to_file = Filename.concat session_dir to_file in
if Sys.file_exists abs_to_file then
let msg = Format.sprintf "File %s should not exist" abs_to_file in
P.notify (Message (Error msg))
else
if not (Sys.file_exists abs_from_file) || Sys.is_directory abs_from_file then
let msg = Format.sprintf "Incorrect file: %s" abs_from_file in
(* Should not happen as this is sent by IDE *)
P.notify (Message (Error msg))
else
begin
C.interrupt ();
Sys.rename abs_from_file abs_to_file;
let msg = "File successfully moved: reloading session..." in
P.notify (Message (Information msg));
(try
(* Ignore the result session because we do not reload *)
let (_: session) = move_file ~shape_version:None ~check_reload:false
d.cont.controller_env s from_file to_file in
let msg = "Filename successfully changed in session" in
P.notify (Message (Information msg))
with _ ->
begin
Sys.rename abs_to_file abs_from_file;
let msg = "Error when changing the session name. Switching filenames back and reload..." in
P.notify (Message (Information msg))
end);
reload_session ();
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 | Check_need_saving_req | Reload_req
| Get_file_contents _ | Save_file_req _
| Interrupt_req | Add_file_req _ | Set_config_param _ | Set_prover_policy _
| Exit_req | Get_global_infos | Itp_communication.Unfocus_req -> true
| Exit_req | Get_global_infos | Itp_communication.Unfocus_req
| Move_source_req _ -> true
| Get_first_unproven_node ni ->
Hint.mem model_any ni
| Remove_subtree nid ->
......@@ -1398,6 +1437,8 @@ end
| Reload_req ->
reload_session ();
session_needs_saving := true
| Move_source_req (from_file, to_file) ->
move_source_file d from_file to_file
| Get_first_unproven_node ni ->
notify_first_unproven_node d ni
| Remove_subtree nid ->
......
......@@ -168,6 +168,7 @@ let convert_request_constructor (r: ide_request) =
| Remove_subtree _ -> String "Remove_subtree"
| Copy_paste _ -> String "Copy_paste"
| Get_first_unproven_node _ -> String "Get_first_unproven_node"
| Move_source_req _ -> String "Move_source_req"
| Unfocus_req -> String "Unfocus_req"
| Save_req -> String "Save_req"
| Check_need_saving_req -> String "Check_need_saving_req"
......@@ -223,6 +224,10 @@ 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]
| Move_source_req (from_file, to_file) ->
convert_record ["ide_request", cc r;
"from_file", String from_file;
"to_file", String to_file]
| Check_need_saving_req
| Unfocus_req
| Save_req
......@@ -456,6 +461,11 @@ let parse_request (constr: string) j =
let nid = get_int (get_field j "node_ID") in
Get_first_unproven_node nid
| "Move_source_req" ->
let from_file = get_string (get_field j "from_file") in
let to_file = get_string (get_field j "to_file") in
Move_source_req (from_file, to_file)
| "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