Commit 1f3e77e2 authored by Sylvain Dailler's avatar Sylvain Dailler Committed by MARCHE Claude

Add move source file in both why3session and API

parent 2172e567
......@@ -840,7 +840,7 @@ install_local:: bin/why3webserver
###############
SESSION_FILES = why3session_lib why3session_info \
why3session_html why3session_latex \
why3session_html why3session_latex why3session_mv \
why3session_main
# TODO: why3session_copy why3session_rm why3session_csv why3session_run
# why3session_output
......
......@@ -73,7 +73,6 @@ let unproven_goals_below_id cont id =
| ATh th ->
List.rev (unproven_goals_below_th cont [] th)
(****** Exception handling *********)
let p s id =
......
......@@ -9,10 +9,6 @@
(* *)
(********************************************************************)
open Wstdlib
module Hprover = Whyconf.Hprover
......@@ -38,7 +34,7 @@ let print_proofAttemptID fmt id =
type theory = {
theory_name : Ident.ident;
mutable theory_goals : proofNodeID list;
theory_parent_name : string;
mutable theory_parent_name : string;
mutable theory_is_detached : bool;
}
......@@ -1612,9 +1608,6 @@ let merge_file_section ~shape_version ~old_ses ~old_theories ~file_is_detached ~
f.file_theories <- theories @ detached;
update_file_node (fun _ -> ()) s f
let read_file env ?format fn =
let theories = Env.read_file Env.base_language env ?format fn in
let ltheories =
......@@ -1948,3 +1941,48 @@ let save_session (s : session) =
session_dir_for_save := s.session_dir;
let fs = if Compress.compression_supported then fz else fs in
save f fs s
(**********************)
(* 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
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
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)
......@@ -282,3 +282,15 @@ val change_prover : notifier -> session -> proofNodeID -> Whyconf.prover -> Whyc
attempt using prover [opr] by the new prover [npr]. Proof attempt
status is set to obsolete.
*)
(** 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.
*)
......@@ -218,3 +218,13 @@ 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,3 +76,10 @@ 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,6 +18,7 @@ let cmds =
Why3session_info.cmd;
Why3session_html.cmd;
Why3session_latex.cmd;
Why3session_mv.cmd_mv;
(*
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;
}
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