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

a few additional fix

parent 06c1a5a5
......@@ -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
......
......@@ -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_path (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_path 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 (fun f -> Sysutil.absolutize_path dirname [f])
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_path (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 (fun f -> Sysutil.absolutize_path dirname [f])
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)) ()
......
......@@ -413,8 +413,9 @@ let get_locations (task: Task.task) =
let relativize f =
try Hstr.find file_cache f
with Not_found ->
(* FIXME: this an abusive use of Sysutil.absolutize_path *)
let g = Sysutil.absolutize_path "" (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 =
......@@ -568,8 +569,9 @@ end
let relativize_location s loc =
let f, l, b, e = Loc.get loc in
(* FIXME: this an abusive use of Sysutil.absolutize_path *)
let f = Sysutil.absolutize_path "" (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 =
......@@ -941,16 +943,16 @@ end
P.notify (Message (Information ("File already in session: " ^ f)))
with Not_found ->
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 add_file cont f with
match l with
| [] ->
session_needs_saving := true;
let file = find_file_from_path cont.controller_session fn in
send_new_subtree_from_file file;
read_and_send (Sysutil.absolutize_path dir fn);
P.notify (Message (Information "file added in session"))
| l ->
read_and_send (Sysutil.absolutize_path dir fn);
List.iter
(function
| (loc,rel_loc,s) ->
......
......@@ -143,7 +143,7 @@ type session = {
}
let system_path s f =
Sysutil.absolutize_path s.session_dir f.file_path
Sysutil.system_dependent_absolute_path s.session_dir f.file_path
let theory_parent s th =
Debug.dprintf debug "[Session_itp.theory_parent] th.parent_name = %d@."
......@@ -1675,7 +1675,7 @@ let read_file env ?format fn =
let merge_file ~shape_version env (ses : session) (old_ses : session) file =
let format = file_format file in
let old_theories = file_theories file in
let file_name = Sysutil.absolutize_path (get_dir old_ses) (file_path file) in
let file_name = Sysutil.system_dependent_absolute_path (get_dir old_ses) (file_path file) in
Debug.dprintf debug "merging file %s@." file_name;
try
let new_theories = read_file env file_name ?format in
......@@ -1944,7 +1944,7 @@ let save_theory s ctxt fmt t =
let save_file s ctxt fmt _ f =
fprintf fmt
"@\n@[<v 0>@[<h><file@ %a%a>@]"
"@\n@[<v 0>@[<h><file%a%a>@]"
(opt_string "format") f.file_format
(save_bool_def "proved" false) (file_proved s f);
List.iter (fun s -> fprintf fmt "@\n@[<hov 1><path@ name=\"%s\"/>@]" s) f.file_path;
......
......@@ -70,7 +70,7 @@ 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 path associated to that file *)
(** the system-dependent absolute path associated to that file *)
val basename : file_path -> string
......
......@@ -102,6 +102,9 @@ 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
let system_independent_path_of_file f =
let rec aux acc f =
let d = Filename.dirname f in
......@@ -118,40 +121,6 @@ let system_independent_path_of_file f =
in
aux [] f
(*
(* 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 absolute_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 ())
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
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)
......@@ -166,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 =
......@@ -208,12 +166,7 @@ let relativize_filename base f =
in
aux [] (system_independent_path_of_file base) (system_independent_path_of_file f)
let absolutize_path dirname p =
let f = file_of_path p in
if Filename.is_relative f then
Filename.concat dirname f
else
f
(*
let p1 = relativize_filename "/bin/bash" "src/f.why"
......
......@@ -52,22 +52,17 @@ val copy_dir : string -> string -> unit
currently the directory must contains only directories and common files
*)
val system_independent_path_of_file : string -> string list
(** [path_of_file filename] return the access path of [filename], in a
system-independent way *)
val concat : string -> string -> string
(** like [Filename.concat] but returns only second string when it is already absolute *)
(*
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 file_of_path : string list -> string
(** [file_of_path path] return the system-dependent textual path for [path] *)
*)
(* unused ?
val normalize_filename : string -> string
*)
(** [normalize_filename filename] removes from [filename] occurrences of
"." and ".." that denote respectively the current directory and
parent directory, whenever possible *)
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
......@@ -75,14 +70,12 @@ val relativize_filename : string -> string -> string list
into path components using the system-dependent calls to
[Filename.dirname] and [Filename.basename].
OBSOLETE? [base] should not contain occurrences of "." and "..",
which can be removed by calling first [normalize_filename]. *)
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
*)
val absolutize_path : string -> string list -> string
(** [absolutize_filename base path] constructs a filename for the
[path] relatively to [base]. The character marking directories in
the result is the one produced by the system-dependent call to
[Filename.concat] *)
val uniquify : string -> string
(** find filename that doesn't exist based on the given filename.
......
......@@ -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 = Sysutil.absolutize_path (Session_itp.get_dir session) src in
let dst = Sysutil.absolutize_path (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