Commit d55ea9b9 authored by MARCHE Claude's avatar MARCHE Claude

fix implementation of 'rename file' feature

parent 28ab37cf
......@@ -840,7 +840,7 @@ install_local:: bin/why3webserver
###############
SESSION_FILES = why3session_lib why3session_info \
why3session_html why3session_latex why3session_mv \
why3session_html why3session_latex why3session_update \
why3session_main
# TODO: why3session_copy why3session_rm why3session_csv why3session_run
# why3session_output
......
......@@ -2241,59 +2241,6 @@ 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) *)
......
......@@ -174,9 +174,9 @@ val reload_files : controller -> shape_version:int option -> bool * bool
*)
val add_file : controller -> ?format:Env.fformat -> string -> unit
(** [add_fil cont ?fmt fname] parses the source file
(** [add_file cont ?fmt fname] parses the source file
[fname] and add the resulting theories to the session of [cont].
parsing or typing errors are raised inside exception Errors_list
parsing or typing errors are raised inside exception [Errors_list]
*)
val remove_subtree: notification:notifier -> removed:notifier ->
......
......@@ -117,7 +117,6 @@ 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
......@@ -145,7 +144,6 @@ 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,9 +135,6 @@ 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,52 +1364,13 @@ 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
| Move_source_req _ -> true
| Exit_req | Get_global_infos | Itp_communication.Unfocus_req -> true
| Get_first_unproven_node ni ->
Hint.mem model_any ni
| Remove_subtree nid ->
......@@ -1437,8 +1398,6 @@ 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,7 +168,6 @@ 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"
......@@ -224,10 +223,6 @@ 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
......@@ -461,11 +456,6 @@ 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
......
......@@ -1946,43 +1946,21 @@ let save_session (s : session) =
(* Edition of session *)
(**********************)
let move_file ~shape_version ~check_reload env ses from_file to_file =
assert (Sys.file_exists (Filename.concat ses.session_dir to_file));
assert (not (Sys.is_directory (Filename.concat ses.session_dir to_file)));
assert (Filename.check_suffix to_file ".mlw");
let files = get_files ses in
let key_from_file =
(* let exception for OCaml prior to version 4.03 *)
let module M = struct exception Found of string end in
let rename_file s from_file to_file =
let src = Sysutil.relativize_filename s.session_dir from_file in
let dst = Sysutil.relativize_filename s.session_dir to_file in
let files = get_files s in
let file =
try
Hstr.iter (fun key file ->
if file.file_name = from_file then
raise (M.Found key)
) files;
None
with M.Found s -> Some s
Hstr.find files src
with Not_found -> failwith ("filename " ^ src ^ " not found in session")
in
match key_from_file with
| None -> raise Not_found
| Some key_file ->
let old_file = Hstr.find files key_file in
Hstr.remove files key_file;
List.iter (fun th -> th.theory_parent_name <- to_file) old_file.file_theories;
let new_file =
{old_file with
file_name = to_file;
file_is_detached = true
}
in
Hstr.add files to_file new_file;
(* Only save the new session if the .mlw file [to_file] does not mess with
the session: parse/type errors, other errors ?
*)
if check_reload then
let new_ses = empty_session ~from:ses (get_dir ses) in
let e_l, _, _ = merge_files ~shape_version env new_ses ses in
match e_l with
| [] -> save_session new_ses; new_ses
| e :: _ -> raise e
else
(save_session ses; ses)
assert (file.file_name = src);
assert (Sys.file_exists (Filename.concat s.session_dir src));
assert (not (Sys.is_directory (Filename.concat s.session_dir src)));
assert (not (Sys.file_exists (Filename.concat s.session_dir dst)));
Sys.rename (Filename.concat s.session_dir src) (Filename.concat s.session_dir dst);
Hstr.remove files src;
List.iter (fun th -> th.theory_parent_name <- dst) file.file_theories;
let new_file = { file with file_name = dst } in
Hstr.add files dst new_file
......@@ -160,13 +160,18 @@ val add_file_section :
(** [add_file_section s fn ths] adds a new
'file' section in session [s], named [fn], containing fresh theory
subsections corresponding to theories [ths]. The tasks of each
theory nodes generated are computed using [Task.split_theory]. *)
theory nodes generated are computed using [Task.split_theory].
Note that this function does not read anything from the file
system. The file name [fn] is taken as is
*)
val read_file :
Env.env -> ?format:Env.fformat -> string -> Theory.theory list
(* [read_file env ~format fn] parses the source file [fn], types it
and extract its theories. Parse errors and typing errors are
signaled with exceptions. *)
and extract its theories. A parse error or a typing error is
signaled with exceptions . *)
val merge_files :
shape_version:int option ->
......@@ -285,12 +290,7 @@ val change_prover : notifier -> session -> proofNodeID -> Whyconf.prover -> Whyc
(** Edition of session *)
val move_file: shape_version:int option -> check_reload:bool -> Env.env ->
session -> string -> string -> session
(** [move_file shape check_reload env s from_file to_file] This changes the
filename in session from [from_file] to [to_file] and reload the session (if
[check_reload] is true) so that the session is up to date with what is
inside the new [to_file].
Returns the current session.
[from_file] and [to_file] are paths given relative to the session directory.
val rename_file: session -> string -> string -> unit
(** [rename_file s from_file to_file] renames the
filename in session from [from_file] to [to_file]
*)
......@@ -218,13 +218,3 @@ let uniquify file =
done;
let file = name ^ "_" ^ (string_of_int !i) ^ ext in
file
let cannonical file =
assert (Sys.file_exists file);
let cwd = Sys.getcwd () in
let file_dir = Filename.dirname file in
Sys.chdir file_dir;
let file_dir = Sys.getcwd () in
(* Return to dir *)
Sys.chdir cwd;
Filename.concat file_dir (Filename.basename file)
......@@ -76,10 +76,3 @@ val uniquify : string -> string
(** find filename that doesn't exists based on the given filename.
Be careful the file can be taken after the return of this function.
*)
val cannonical : string -> string
(** Give a cannonical name to an existing file. Done by chdir to this files
directory and getting the current working directory from there.
TODO: find a better solution that works with both non-existing files, all
OS, and potential symbolic links in filesystems.
*)
......@@ -18,7 +18,7 @@ let cmds =
Why3session_info.cmd;
Why3session_html.cmd;
Why3session_latex.cmd;
Why3session_mv.cmd_mv;
Why3session_update.cmd_update;
(*
Why3session_csv.cmd;
Why3session_copy.cmd_mod;
......
open Why3
open Why3session_lib
open Session_itp
let from_file = ref ""
let to_file = ref ""
let spec_mv =
("-i", Arg.String (fun s -> from_file := s),
"<file> file to move") ::
("-o", Arg.String (fun s -> to_file := s),
"<file> path to move to") ::
common_options
let move ~env ~session from_file to_file =
let dir = Filename.dirname session in
let from_file = Sysutil.relativize_filename dir (Sysutil.cannonical from_file) in
let to_file = Sysutil.relativize_filename dir (Sysutil.cannonical to_file) in
(* TODO match exceptions ? *)
let session, shape_version = load_session dir in
let (_: session) = move_file ~shape_version ~check_reload:true env session from_file to_file in
()
let run_mv () =
let env,_config,should_exit1 = read_env_spec () in
if should_exit1 || !from_file = "" || !to_file = "" then exit 1;
iter_files (fun session -> move ~env ~session !from_file !to_file)
let cmd_mv =
{ cmd_spec = spec_mv;
cmd_desc = "change an .mlw file in the session to another .mlw file";
cmd_name = "mv";
cmd_run = run_mv;
}
open Why3
open Why3session_lib
type action = RenameFile of string * string
let actions = ref ([] : action list)
let spec_update =
let from_file = ref "" in
("-rename-file",
Arg.(Tuple [Set_string from_file;
String (fun s -> actions := RenameFile(!from_file,s) :: !actions)]),
"<oldname> <newname> rename file") ::
common_options
let do_action ~env ~session action =
ignore(env);
match action with
| RenameFile(src,dst) ->
Session_itp.rename_file session src dst
let run_update () =
let env,_config,should_exit1 = read_env_spec () in
if should_exit1 then exit 1;
iter_files
(fun fname ->
let session, _ = read_session fname in
List.iter (do_action ~env ~session) !actions;
Session_itp.save_session session)
let cmd_update =
{ cmd_spec = spec_update;
cmd_desc = "update session from the command line";
cmd_name = "update";
cmd_run = run_update;
}
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