Commit 7e0feeac authored by Sylvain Dailler's avatar Sylvain Dailler Committed by MARCHE Claude

WIP: TODO to check, amend and squash

rename_file: change behavior and properly remove ide related stuff.
parent 1eb33ff3
......@@ -372,9 +372,6 @@ 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 =
......@@ -384,7 +381,6 @@ 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;
......@@ -2142,10 +2138,6 @@ 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 () =
......@@ -2241,7 +2233,6 @@ let () =
connect_menu_item copy_item ~callback:copy;
connect_menu_item paste_item ~callback:paste
(**********************************)
(* Notification handling (part 2) *)
(**********************************)
......
......@@ -1956,11 +1956,8 @@ let rename_file s from_file to_file =
with Not_found -> failwith ("filename " ^ src ^ " not found in session")
in
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
Hstr.add files dst new_file;
src,dst
......@@ -290,7 +290,8 @@ val change_prover : notifier -> session -> proofNodeID -> Whyconf.prover -> Whyc
(** Edition of session *)
val rename_file: session -> string -> string -> unit
val rename_file: session -> string -> string -> string * string
(** [rename_file s from_file to_file] renames the
filename in session from [from_file] to [to_file]
@return the paths relative to the session dir
*)
......@@ -18,7 +18,13 @@ let do_action ~env ~session action =
ignore(env);
match action with
| RenameFile(src,dst) ->
Session_itp.rename_file session src dst
let src,dst = Session_itp.rename_file session src dst in
let src = Filename.concat (Session_itp.get_dir session) src in
let dst = Filename.concat (Session_itp.get_dir session) dst in
assert (Sys.file_exists src);
assert (not (Sys.is_directory src));
assert (not (Sys.file_exists dst));
Sys.rename src dst
let run_update () =
let env,_config,should_exit1 = read_env_spec () in
......
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