Commit 72ead311 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch '247-make-file-paths-in-sessions-system-independant' into 'master'

Resolve "Make file paths in sessions system-independant"

Closes #247

See merge request !71
parents b7c7893b 72e81dd7
......@@ -4,11 +4,15 @@
<why3session shape_version="5">
<prover id="0" name="Z3" version="4.6.0" timelimit="11" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="11" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="11" steplimit="0" memlimit="1000"/>
<file name="../isqrt.mlw" proved="true">
<file proved="true">
<path name=".."/>
<path name="isqrt.mlw"/>
<theory name="Square" proved="true">
<goal name="sqr_non_neg" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="sqr_increasing" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
......
......@@ -73,7 +73,8 @@ let file : Session_itp.file =
let file_name = "examples/logic/hello_proof.why" in
try
Controller_itp.add_file controller file_name;
Session_itp.get_file session file_name
let path = Sysutil.relativize_filename (Session_itp.get_dir session) file_name in
Session_itp.find_file_from_path session path
with
| Controller_itp.Errors_list le ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" file_name
......
......@@ -10,11 +10,14 @@
<!ATTLIST prover memlimit CDATA #IMPLIED>
<!ATTLIST prover steplimit CDATA #IMPLIED>
<!ELEMENT file (theory*)>
<!ATTLIST file name CDATA #REQUIRED>
<!ELEMENT file (path*) (theory*)>
<!ATTLIST file name CDATA #IMPLIED>
<!ATTLIST file verified CDATA #IMPLIED>
<!ATTLIST file proved CDATA #IMPLIED>
<!ELEMENT path EMPTY>
<!ATTLIST path name CDATA #REQUIRED>
<!ELEMENT theory (label*,goal*)>
<!ATTLIST theory name CDATA #REQUIRED>
<!ATTLIST theory verified CDATA #IMPLIED>
......
......@@ -514,7 +514,7 @@ let call_on_buffer ~command ~limit ~res_parser ~filename ~printer_mapping
Filename.open_temp_file "why_" ("_" ^ filename)
else
begin
let filename = Sysutil.absolutize_filename (Sys.getcwd ()) filename in
let filename = Sysutil.concat (Sys.getcwd ()) filename in
if inplace then
Sys.rename filename (backup_file filename);
filename, open_out filename
......
......@@ -123,7 +123,7 @@ rule token = parse
match tok with
| INPUT filename ->
let dirname = Filename.dirname lexbuf.lex_curr_p.pos_fname in
let filename = Sysutil.absolutize_filename dirname filename in
let filename = Sysutil.concat dirname filename in
Stack.push (input_lexbuf filename) s;
multifile lex_dumb
| EOF -> ignore (Stack.pop s);
......
......@@ -530,7 +530,7 @@ let load_main dirname section =
raise WrongMagicNumber;
{ libdir = get_string ~default:default_main.libdir section "libdir";
datadir = get_string ~default:default_main.datadir section "datadir";
loadpath = List.map (Sysutil.absolutize_filename dirname)
loadpath = List.map (Sysutil.concat dirname)
(get_stringl ~default:[] section "loadpath");
timelimit = get_int ~default:default_main.timelimit section "timelimit";
memlimit = get_int ~default:default_main.memlimit section "memlimit";
......@@ -556,7 +556,7 @@ let read_config_rc conf_file =
exception ConfigFailure of string (* filename *) * string
let get_dirname filename =
Filename.dirname (Sysutil.absolutize_filename (Sys.getcwd ()) filename)
Filename.dirname (Sysutil.concat (Sys.getcwd ()) filename)
let get_config (filename,rc) =
let dirname = get_dirname filename in
......@@ -688,7 +688,7 @@ let merge_config config filename =
let main = match get_section rc "main" with
| None -> config.main
| Some rc ->
let loadpath = (List.map (Sysutil.absolutize_filename dirname)
let loadpath = (List.map (Sysutil.concat dirname)
(get_stringl ~default:[] rc "loadpath")) @ config.main.loadpath in
let plugins =
(get_stringl ~default:[] rc "plugin") @ config.main.plugins in
......
......@@ -678,7 +678,8 @@ let create_source_view =
let create_source_view f content =
if not (Hstr.mem source_view_table f) then
begin
let label = GMisc.label ~text:f () in
let label = GMisc.label ~text:(Filename.basename f) () in
label#misc#set_tooltip_markup f;
let source_page, scrolled_source_view =
!n, GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
......
......@@ -176,9 +176,9 @@ module PSession = struct
let s = x.tcont.controller_session in
let n y acc = { x with tkind = y } :: acc in
match x.tkind with
| Session -> "", Hstr.fold (fun _ f -> n (File f)) (get_files s) []
| Session -> "", Hfile.fold (fun _ f -> n (File f)) (get_files s) []
| File f ->
(file_name f),
string_of_file_path (file_path f),
List.fold_right (fun th -> n (Theory th)) (file_theories f) []
| Theory th ->
let id = theory_name th in
......@@ -607,12 +607,14 @@ let create_file_rel_path c pr pn =
let th = get_encapsulating_theory session (APn pn) in
let th_name = (Session_itp.theory_name th).Ident.id_string in
let f = get_encapsulating_file session (ATh th) in
let fn = Filename.chop_extension (Filename.basename (file_name f)) in
let fn = Filename.chop_extension (Session_itp.basename (file_path f)) in
let file = Driver.file_of_task driver fn th_name task in
let file = Filename.concat session_dir file in
let file = Sysutil.uniquify file in
let file = Sysutil.relativize_filename session_dir file in
file
match file with
| [f] -> f
| _ -> assert false
let prepare_edition c ?file pn pr ~notification =
let session = c.controller_session in
......
......@@ -348,13 +348,13 @@ let () =
let pn_to_node_ID : node_ID Hpn.t = Hpn.create 17
let tn_to_node_ID : node_ID Htn.t = Htn.create 17
let th_to_node_ID : node_ID Ident.Hid.t = Ident.Hid.create 7
let file_to_node_ID : node_ID Hstr.t = Hstr.create 3
let file_to_node_ID : node_ID Hfile.t = Hfile.create 3
let node_ID_from_pan pan = Hpan.find pan_to_node_ID pan
let node_ID_from_pn pn = Hpn.find pn_to_node_ID pn
let node_ID_from_tn tn = Htn.find tn_to_node_ID tn
let node_ID_from_th th = Ident.Hid.find th_to_node_ID (theory_name th)
let node_ID_from_file file = Hstr.find file_to_node_ID (file_name file)
let node_ID_from_file file = Hfile.find file_to_node_ID (file_id file)
let node_ID_from_any any =
match any with
......@@ -367,9 +367,9 @@ let () =
let remove_any_node_ID any =
match any with
| AFile file ->
let nid = Hstr.find file_to_node_ID (file_name file) in
let nid = Hfile.find file_to_node_ID (file_id file) in
Hint.remove model_any nid;
Hstr.remove file_to_node_ID (file_name file)
Hfile.remove file_to_node_ID (file_id file)
| ATh th ->
let nid = Ident.Hid.find th_to_node_ID (theory_name th) in
Hint.remove model_any nid;
......@@ -389,7 +389,7 @@ let () =
let add_node_to_table node new_id =
match node with
| AFile file -> Hstr.add file_to_node_ID (file_name file) new_id
| AFile file -> Hfile.add file_to_node_ID (file_id file) new_id
| ATh th -> Ident.Hid.add th_to_node_ID (theory_name th) new_id
| ATn tn -> Htn.add tn_to_node_ID tn new_id
| APn pn -> Hpn.add pn_to_node_ID pn new_id
......@@ -413,7 +413,9 @@ let get_locations (task: Task.task) =
let relativize f =
try Hstr.find file_cache f
with Not_found ->
let g = Sysutil.relativize_filename session_dir f in
let path = Sysutil.relativize_filename session_dir f in
(* FIXME: this an abusive use of Sysutil.system_dependent_absolute_path *)
let g = Sysutil.system_dependent_absolute_path "" path in
Hstr.replace file_cache f g;
g in
let color_loc ~color ~loc =
......@@ -543,27 +545,33 @@ end
try
let d = get_server_data() in
if d.send_source then
let fn = Sysutil.absolutize_filename
(*
let fn = Sysutil.absolutize_path
(Session_itp.get_dir d.cont.controller_session) f in
let s = Sysutil.file_contents fn in
*)
let s = Sysutil.file_contents f in
P.notify (File_contents (f, s))
with Invalid_argument s ->
P.notify (Message (Error s))
let save_file f file_content =
try
(*
let d = get_server_data() in
let fn = Sysutil.absolutize_filename
(Session_itp.get_dir d.cont.controller_session) f in
Sysutil.backup_file fn;
Sysutil.write_file fn file_content;
*)
Sysutil.backup_file f;
Sysutil.write_file f file_content;
P.notify (Message (File_Saved f))
with Invalid_argument s ->
P.notify (Message (Error s))
let relativize_location s loc =
let f, l, b, e = Loc.get loc in
let f = Sysutil.relativize_filename (Session_itp.get_dir s) f in
let path = Sysutil.relativize_filename (Session_itp.get_dir s) f in
(* FIXME: this an abusive use of Sysutil.system_dependent_absolute_path *)
let f = Sysutil.system_dependent_absolute_path "" path in
Loc.user_position f l b e
let capture_parse_or_type_errors f cont =
......@@ -608,7 +616,7 @@ end
let get_node_name (node: any) =
let d = get_server_data () in
match node with
| AFile file -> file_name file
| AFile file -> Session_itp.basename (file_path file)
| ATh th -> (theory_name th).Ident.id_string
| ATn tn ->
let name = get_transf_name d.cont.controller_session tn in
......@@ -787,7 +795,7 @@ end
let d = get_server_data () in
let ses = d.cont.controller_session in
let files = get_files ses in
Hstr.iter
Hfile.iter
(fun _ file ->
on_file file;
iter_subtree_from_file on_subtree file)
......@@ -807,9 +815,12 @@ end
let reset_and_send_the_whole_tree (): unit =
P.notify Reset_whole_tree;
iter_on_files
~on_file:(fun file -> read_and_send (file_name file))
~on_subtree:create_node
let d = get_server_data () in
let ses = d.cont.controller_session in
let on_file f =
read_and_send (Session_itp.system_path ses f)
in
iter_on_files ~on_file ~on_subtree:create_node
let unfocus () =
focused_node := Unfocused;
......@@ -830,12 +841,10 @@ end
let create_ce_tab ~print_attrs s res any list_loc =
let f = get_encapsulating_file s any in
let filename = Sysutil.absolutize_filename
(Session_itp.get_dir s) (file_name f)
in
let filename = Session_itp.system_path s f in
let source_code = Sysutil.file_contents filename in
Model_parser.interleave_with_source ~print_attrs ?start_comment:None ?end_comment:None
?me_name_trans:None res.Call_provers.pr_model ~rel_filename:(file_name f)
?me_name_trans:None res.Call_provers.pr_model ~rel_filename:filename
~source_code:source_code ~locations:list_loc
let send_task nid show_full_context loc =
......@@ -858,7 +867,7 @@ end
let prover_text = "Detached prover\n====================> Prover: " ^ name ^ "\n" in
P.notify (Task (nid, prover_text, []))
| AFile f ->
P.notify (Task (nid, "Detached file " ^ file_name f, []))
P.notify (Task (nid, "Detached file " ^ (basename (file_path f)), []))
| ATn tid ->
let name = get_transf_name d.cont.controller_session tid in
let args = get_transf_args d.cont.controller_session tid in
......@@ -909,7 +918,7 @@ end
| None -> P.notify (Task (nid, "Result of the prover not available.\n", old_list_loc))
end
| AFile f ->
P.notify (Task (nid, "File " ^ file_name f, []))
P.notify (Task (nid, "File " ^ (basename (file_path f)), []))
| ATn tid ->
let name = get_transf_name d.cont.controller_session tid in
let args = get_transf_args d.cont.controller_session tid in
......@@ -927,31 +936,31 @@ end
(* Note that f is the path from execution directory to the file and fn is the
path from the session directory to the file. *)
let add_file_to_session cont f =
let fn = Sysutil.relativize_filename
(get_dir cont.controller_session) f in
let dir = get_dir cont.controller_session in
let fn = Sysutil.relativize_filename dir f in
try
let (_ : file) = get_file cont.controller_session fn in
P.notify (Message (Information ("File already in session: " ^ fn)))
let (_ : file) = find_file_from_path cont.controller_session fn in
P.notify (Message (Information ("File already in session: " ^ f)))
with Not_found ->
if (Sys.file_exists f) then
begin
match add_file cont f with
| [] ->
if (Sys.file_exists f) then
let l = add_file cont f in
let file = find_file_from_path cont.controller_session fn in
send_new_subtree_from_file file;
read_and_send (Session_itp.system_path cont.controller_session file);
begin
match l with
| [] ->
session_needs_saving := true;
let file = get_file cont.controller_session fn in
send_new_subtree_from_file file;
read_and_send (file_name file);
P.notify (Message (Information "file added in session"))
| l ->
read_and_send fn;
List.iter
(function
| (loc,rel_loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s))))
l
end
else
P.notify (Message (Open_File_Error ("File not found: " ^ f)))
P.notify (Message (Information "file added in session"))
| l ->
List.iter
(function
| (loc,rel_loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s))))
l
end
else
P.notify (Message (Open_File_Error ("File not found: " ^ f)))
(* ------------ init server ------------ *)
......@@ -1266,7 +1275,7 @@ end
Hpn.clear pn_to_node_ID;
Htn.clear tn_to_node_ID;
Ident.Hid.clear th_to_node_ID;
Hstr.clear file_to_node_ID
Hfile.clear file_to_node_ID
let reload_session () : unit =
let d = get_server_data () in
......
This diff is collapsed.
......@@ -31,11 +31,16 @@ val print_proofNodeID : Format.formatter -> proofNodeID -> unit
type transID
type proofAttemptID
val print_proofAttemptID : Format.formatter -> proofAttemptID -> unit
type fileID
module Hfile: Exthtbl.S with type key = fileID
module Hpn: Exthtbl.S with type key = proofNodeID
module Htn: Exthtbl.S with type key = transID
module Hpan: Exthtbl.S with type key = proofAttemptID
type file_path
val string_of_file_path : file_path -> string
val print_file_path : Format.formatter -> file_path -> unit
(* Any proof node of the tree *)
type any =
......@@ -53,16 +58,21 @@ type notifier = any -> unit
(** Session *)
(* Get all the files in the session *)
val get_files : session -> file Wstdlib.Hstr.t
val get_files : session -> file Hfile.t
(* Get a single file in the session using its name *)
val get_file: session -> string -> file
(* val get_file: session -> string -> file *)
(* Get directory containing the session *)
val get_dir : session -> string
(** File *)
val file_name : file -> string
val file_id : file -> fileID
val file_path : file -> file_path
val file_format : file -> string option
val file_theories : file -> theory list
val system_path : session -> file -> string
(** the system-dependent absolute path associated to that file *)
val basename : file_path -> string
(** Theory *)
val theory_name : theory -> Ident.ident
......@@ -290,7 +300,10 @@ val change_prover : notifier -> session -> proofNodeID -> Whyconf.prover -> Whyc
(** Extra session update operations *)
val rename_file: session -> string -> string -> string * string
val find_file_from_path: session -> string list -> file
(** raise [Not_found] of path does not appear in session *)
val rename_file: session -> string -> string -> (string list) * (string list)
(** [rename_file s from_file to_file] renames the
file section in session [s] named [from_file] into [to_file]
@return the paths relative to the session dir
......
......@@ -149,7 +149,7 @@ let print_statistics ses files =
in
let print_file (f,ths,n,m) =
if n<m then begin
printf " +--file %s: %d/%d@." (S.file_name f) n m;
printf " +--file [%a]: %d/%d@." S.print_file_path (S.file_path f) n m;
List.iter print_theory (List.rev ths)
end
in
......@@ -207,7 +207,7 @@ let run_replay some_merge_miss found_obs cont =
let final_callback found_upgraded_prover report =
Debug.dprintf debug "@.";
let files,n,m =
Wstdlib.Hstr.fold (file_statistics session)
S.Hfile.fold (file_statistics session)
(S.get_files session) ([],0,0)
in
let report =
......
......@@ -102,38 +102,25 @@ let rec copy_dir from to_ =
else copy_file src dst in
Array.iter copy files
let concat f1 f2 =
if Filename.is_relative f2 then Filename.concat f1 f2 else f2
(* return the absolute path of a given file name.
this code has been designed to be architecture-independant so
be very careful if you modify this *)
let path_of_file f =
let system_independent_path_of_file f =
let rec aux acc f =
(*
Format.printf "aux %s@." f;
let _ = read_line () in
*)
let d = Filename.dirname f in
if d = Filename.current_dir_name then
(* f is relative to the current dir *)
let b = Filename.basename f in
aux (b::acc) (Sys.getcwd ())
b::acc
else if f=d then
(* we are at the root *)
acc
else
let b = Filename.basename f in
if f=b then b::acc else
aux (b::acc) d
aux (b::acc) d
in
aux [] f
(* return the file name of an absolute path *)
let rec file_of_path l =
match l with
| [] -> ""
| [x] -> x
| x::l -> Filename.concat x (file_of_path l)
(*
let test x = (Filename.dirname x, Filename.basename x)
......@@ -148,26 +135,15 @@ let p1 = path_of_file "/bin/bash"
let p1 = path_of_file "../src/f.why"
*)
(*
let normalize_filename f =
let rec aux af acc =
match af, acc with
| x::rf, _ ->
if x = Filename.current_dir_name then
aux rf acc
else if x = Filename.parent_dir_name then
(match acc with
| _::racc -> aux rf racc
| [] ->
(* do not treat currently cases like "../../../a/b/c/d",
that cannot occur if [f] is a full path *)
failwith "cannot normalize filename")
else
aux rf (x::acc)
| [], _ -> acc
let system_dependent_absolute_path dir p =
let rec file_of_path l =
match l with
| [] -> ""
| [x] -> x
| x::l -> Filename.concat x (file_of_path l)
in
file_of_path (List.rev (aux (path_of_file f) []))
*)
let f = file_of_path p in
Filename.concat dir f
let relativize_filename base f =
let rec aux abs ab af =
......@@ -188,13 +164,9 @@ let relativize_filename base f =
aux2 (x::abs) (Filename.parent_dir_name::rel) rb)
in aux2 abs af ab
in
file_of_path (aux [] (path_of_file base) (path_of_file f))
aux [] (system_independent_path_of_file base) (system_independent_path_of_file f)
let absolutize_filename dirname f =
if Filename.is_relative f then
Filename.concat dirname f
else
f
(*
let p1 = relativize_filename "/bin/bash" "src/f.why"
......
......@@ -52,27 +52,32 @@ val copy_dir : string -> string -> unit
currently the directory must contains only directories and common files
*)
val path_of_file : string -> string list
(** [path_of_file filename] return the absolute path of [filename] *)
val concat : string -> string -> string
(** like [Filename.concat] but returns only second string when it is already absolute *)
(* unused ?
val normalize_filename : string -> string
val system_independent_path_of_file : string -> string list
(** [system_independent_path_of_file filename] return the access path
of [filename], in a system-independent way *)
val system_dependent_absolute_path : string -> string list -> string
(** [system_dependent_absolute_path d p] returns the
system-dependent absolute path for the abstract path [p] relative
to directory [d] *)
val relativize_filename : string -> string -> string list
(** [relativize_filename base filename] returns an access path for
filename [filename] relatively to [base]. The [filename] is split
into path components using the system-dependent calls to
[Filename.dirname] and [Filename.basename].
OBSOLETE COMMENT? [base] should not contain occurrences of "." and "..",
which can be removed by calling first [normalize_filename].
FIXME: this function does not handle symbolic links properly
*)
(** [normalize_filename filename] removes from [filename] occurrences of
"." and ".." that denote respectively the current directory and
parent directory, whenever possible *)
val relativize_filename : string -> string -> string
(** [relativize_filename base filename] relativize the filename
[filename] according to [base]. [base] should not contain occurrences of
"." and "..", which can be removed by calling first [normalize_filename].
*)
val absolutize_filename : string -> string -> string
(** [absolutize_filename base filename] absolutize the filename
[filename] according to [base] *)
val uniquify : string -> string
(** find filename that doesn't exists based on the given filename.
(** find filename that doesn't exist based on the given filename.
Be careful the file can be taken after the return of this function.
*)
......@@ -11,7 +11,6 @@
open Format
open Why3
open Wstdlib
open Why3session_lib
module Hprover = Whyconf.Hprover
......@@ -220,7 +219,7 @@ let rec num_lines s acc tr =
let print_file s fmt f =
(* fprintf fmt "<h1>File %s</h1>@\n" f.file_name; *)
let fn = Filename.basename (file_name f) in
let fn = basename (file_path f) in
let fn = Filename.chop_extension fn in
fprintf fmt "%a"
(Pp.print_list Pp.newline (print_theory s fn)) (file_theories f)
......@@ -228,7 +227,7 @@ let rec num_lines s acc tr =
let print_session name fmt s =
fprintf fmt "<h1>Why3 Proof Results for Project \"%s\"</h1>@\n" name;
fprintf fmt "%a"
(Pp.print_iter2 Hstr.iter Pp.newline Pp.nothing Pp.nothing
(Pp.print_iter2 Hfile.iter Pp.newline Pp.nothing Pp.nothing
(print_file s)) (get_files s)
end
......@@ -274,13 +273,13 @@ struct
(print_ul (print_goal s)) (theory_goals th)
let print_file s fmt f =
fprintf fmt "<li>%s%a</li>"
(file_name f)
fprintf fmt "<li>%a%a</li>"
print_file_path (file_path f)
(print_ul (print_theory s)) (file_theories f)
let print_session _name fmt s =
fprintf fmt "<ul>%a</ul>"
(Pp.print_iter2 Hstr.iter Pp.newline Pp.nothing Pp.nothing
(Pp.print_iter2 Hfile.iter Pp.newline Pp.nothing Pp.nothing
(print_file s)) (get_files s)
end
......
......@@ -187,8 +187,8 @@ and stats_of_transf prefix_name stats ses transf =
let stats_of_theory file stats ses theory =
let goals = theory_goals theory in
let prefix_name = file_name file ^ " / " ^ (theory_name theory).Ident.id_string
^ " / " in
let prefix_name = string_of_file_path (file_path file) ^ " / " ^
(theory_name theory).Ident.id_string ^ " / " in
List.iter (stats_of_goal ~root:true prefix_name stats ses) goals
let stats_of_file stats ses _ file =
......@@ -285,7 +285,7 @@ let stats2_of_file ~nb_proofs ses file =
[] (file_theories file)
let stats2_of_session ~nb_proofs ses acc =
Hstr.fold
Hfile.fold
(fun _ f acc ->
match stats2_of_file ~nb_proofs ses f with
| [] -> acc
......@@ -293,7 +293,7 @@ let stats2_of_session ~nb_proofs ses acc =
(get_files ses) acc
let print_file_stats ~time ses (f,r) =
printf "+-- file %s@\n" (file_name f);
printf "+-- file [%a]@\n" print_file_path (file_path f);
List.iter (print_theory_stats ~time ses) r
let print_session_stats ~time ses = List.iter (print_file_stats ~time ses)
......@@ -373,7 +373,7 @@ let run_one stats r0 r1 fname =
if !opt_stats_print || !opt_hist_print then
begin
(* fill_prover_data stats session; *)
Hstr.iter (stats_of_file stats ses) (get_files ses);
Hfile.iter (stats_of_file stats ses) (get_files ses);
r0 := stats2_of_session ~nb_proofs:0 ses !r0;
r1 := stats2_of_session ~nb_proofs:1 ses !r1
end;
......
......@@ -11,7 +11,6 @@
open Format
open Why3
open Wstdlib
open Session_itp
open Why3session_lib
......@@ -361,7 +360,7 @@ let file_latex_stat_all n s _table dir f =
provers [] in
let provers = List.sort Whyconf.Prover.compare provers in
let depth = file_depth s f in
let name = Filename.basename (file_name f) in
let name = basename (file_path f) in
let ch = open_out (Filename.concat dir(name^".tex")) in
let fmt = formatter_of_out_channel ch in
latex_tabular_file n s fmt depth provers f;
......@@ -423,9 +422,9 @@ let element_latex_stat files n s table dir e =
| [] -> ()
| f :: r ->
let found = ref false in
Hstr.iter
(fun fname file ->
let fname = Filename.basename fname in
Hfile.iter
(fun _ file ->
let fname = basename (file_path file) in
let fname = List.hd (Strings.split '.' fname) in
if fname = f then
begin
......@@ -440,7 +439,7 @@ let print_latex_statistics n table dir session =
let files = get_files session in
match !opt_elements with
| None ->
Hstr.iter (fun _ f -> file_latex_stat n session table dir f) files
Hfile.iter (fun _ f -> file_latex_stat n session table dir f) files
| Some l ->
List.iter (element_latex_stat files n session table dir) l
......
......@@ -18,13 +18,14 @@ let do_action ~env ~session action =
ignore(env);
match action with
| RenameFile(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 src,dst = Session_itp.rename_file session src dst in
let dir = Session_itp.get_dir session in
let src = Sysutil.system_dependent_absolute_path dir src in
let dst = Sysutil.system_dependent_absolute_path dir 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