Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de

chemin physique : expansion uniquement pour Load, Add LoadPath, Declare ML
Module, Cd, ... mais pas pour les options -I, -boot, -R, -load-vernac-file, ...


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9398 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 48 insertions, 49 deletions

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 38ae32912..0278a16cd 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -315,14 +315,14 @@ let parse_file_action reqid file_name =
 		   fnl () ++ Cerrors.explain_exn e));;
 
 let add_rec_path_action reqid string_arg ident_arg =
-  let directory_name = glob string_arg in
+  let directory_name = expand_path_macros string_arg in
     begin
       add_rec_path directory_name (Libnames.dirpath_of_string ident_arg)
     end;;
 	
 
 let add_path_action reqid string_arg =
-  let directory_name = glob string_arg in
+  let directory_name = expand_path_macros string_arg in
     begin
       add_path directory_name Names.empty_dirpath
     end;;
diff --git a/lib/system.ml b/lib/system.ml
index b3c12f705..20c8a84b4 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -43,7 +43,7 @@ let rec expand_macros s i =
 	  let v = safe_getenv (String.sub s (i+1) (n-i-1)) in
 	  let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in
 	  expand_macros s (i + String.length v)
-      | '~' ->
+      | '~' when i = 0 ->
 	  let n = expand_atom s (i+1) in
 	  let v =
 	    if n=i+1 then home
@@ -53,7 +53,7 @@ let rec expand_macros s i =
 	  expand_macros s (String.length v)
       | c -> expand_macros s (i+1)
 
-let glob s = expand_macros s 0
+let expand_path_macros s = expand_macros s 0
 
 (* Files and load path. *)
 
@@ -97,51 +97,44 @@ let all_subdirs ~unix_path:root =
    end ;
   List.rev !l
 
-let search_in_path path filename =
+let where_in_path path filename =
   let rec search = function
     | lpe :: rem ->
-	let f = glob (Filename.concat lpe filename) in
+	let f = Filename.concat lpe filename in
 	if Sys.file_exists f then (lpe,f) else search rem
     | [] ->
 	raise Not_found
   in
   search path
 
-let where_in_path = search_in_path
-
-let find_file_in_path paths name =
-  let globname = glob name in
-  if not (Filename.is_implicit globname) then
-    let root = Filename.dirname globname in
-    root, globname
+let find_file_in_path paths filename =
+  if not (Filename.is_implicit filename) then
+    let root = Filename.dirname filename in
+    root, filename
   else 
-    try 
-      search_in_path paths name
+    try where_in_path paths filename
     with Not_found ->
       errorlabstrm "System.find_file_in_path"
-	(hov 0 (str "Can't find file" ++ spc () ++ str name ++ spc () ++ 
+	(hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ 
 		str "on loadpath"))
 
 let is_in_path lpath filename =
-  try
-    let _ = search_in_path lpath filename in true
-  with
-    Not_found -> false
+  try ignore (where_in_path lpath filename); true
+  with Not_found -> false
 
 let make_suffix name suffix =
   if Filename.check_suffix name suffix then name else (name ^ suffix)
 
-let file_readable_p na =
-  try access (glob na) [R_OK];true with Unix_error (_, _, _) -> false
+let file_readable_p name =
+  try access name [R_OK];true with Unix_error (_, _, _) -> false
 
-let open_trapping_failure open_fun name suffix =
-  let rname = glob (make_suffix name suffix) in
-  try open_fun rname with _ -> error ("Can't open " ^ rname)
+let open_trapping_failure name =
+  try open_out_bin name with _ -> error ("Can't open " ^ name)
 
-let try_remove f =
-  try Sys.remove f
+let try_remove filename =
+  try Sys.remove filename
   with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++
-                   str f ++ str" which is corrupted!" )
+                   str filename ++ str" which is corrupted!" )
 
 let marshal_out ch v = Marshal.to_channel ch v []
 let marshal_in ch =
@@ -152,14 +145,14 @@ exception Bad_magic_number of string
 
 let raw_extern_intern magic suffix =
   let extern_state name = 
-    let (_,channel) as filec =
-      open_trapping_failure (fun n -> n,open_out_bin n) name suffix in
+    let filename = make_suffix name suffix in
+    let channel = open_trapping_failure filename in
     output_binary_int channel magic;
-    filec
-  and intern_state fname = 
-    let channel = open_in_bin fname in
+    filename,channel
+  and intern_state filename = 
+    let channel = open_in_bin filename in
     if input_binary_int channel <> magic then
-      raise (Bad_magic_number fname);
+      raise (Bad_magic_number filename);
     channel
   in 
   (extern_state,intern_state)
@@ -168,17 +161,17 @@ let extern_intern magic suffix =
   let (raw_extern,raw_intern) = raw_extern_intern magic suffix in
   let extern_state name val_0 = 
     try
-      let (fname,channel) = raw_extern name in
+      let (filename,channel) = raw_extern name in
       try
         marshal_out channel val_0;
         close_out channel
       with e -> 
-	begin try_remove fname; raise e end
+	begin try_remove filename; raise e end
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name = 
     try
-      let _,fname = find_file_in_path paths (make_suffix name suffix) in
-      let channel = raw_intern fname in
+      let _,filename = find_file_in_path paths (make_suffix name suffix) in
+      let channel = raw_intern filename in
       let v = marshal_in channel in
       close_in channel; 
       v
diff --git a/lib/system.mli b/lib/system.mli
index d003a1649..1292ec77d 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -26,7 +26,7 @@ val string_of_physical_path : physical_path -> string
 val make_suffix : string -> string -> string
 val file_readable_p : string -> bool
 
-val glob : string -> string
+val expand_path_macros : string -> string
 val getenv_else : string -> string -> string
 val home : string
 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 4449137e8..591b7b5a8 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -42,9 +42,8 @@ open Vernacinterp
 
 (* This path is where we look for .cmo *)
 let coq_mlpath_copy = ref ["."]
-let keep_copy_mlpath s = 
-  let dir = glob s in
-  coq_mlpath_copy := dir :: !coq_mlpath_copy
+let keep_copy_mlpath path = 
+  coq_mlpath_copy := path :: !coq_mlpath_copy
 
 (* If there is a toplevel under Coq *)
 type toplevel = { 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 746a9a9f4..185bfd93c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -119,6 +119,7 @@ let pr_new_syntax loc ocom =
 let rec vernac_com interpfun (loc,com) =
   let rec interp = function
     | VernacLoad (verbosely, fname) ->
+	let fname = expand_path_macros fname in
         (* translator state *)
         let ch = !chan_translate in
         let cs = Lexer.com_state() in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5ae3998f3..db30d7b95 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -597,28 +597,34 @@ let vernac_proof_instr instr =
 (* Auxiliary file management *)
 
 let vernac_require_from export spec filename =
-  Library.require_library_from_file None filename export
+  Library.require_library_from_file None
+    (System.expand_path_macros filename)
+    export
 
 let vernac_add_loadpath isrec pdir ldiropt =
+  let pdir = System.expand_path_macros pdir in
   let alias = match ldiropt with
     | None -> Nameops.default_root_prefix
     | Some ldir -> ldir in
   (if isrec then Mltop.add_rec_path else Mltop.add_path) pdir alias
 
-let vernac_remove_loadpath = Library.remove_load_path
+let vernac_remove_loadpath path =
+  Library.remove_load_path (System.expand_path_macros path)
 
   (* Coq syntax for ML or system commands *)
 
-let vernac_add_ml_path isrec s =
-  (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (System.glob s)
+let vernac_add_ml_path isrec path =
+  (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir)
+    (System.expand_path_macros path)
 
-let vernac_declare_ml_module l = Mltop.declare_ml_modules l
+let vernac_declare_ml_module l =
+  Mltop.declare_ml_modules (List.map System.expand_path_macros l)
 
 let vernac_chdir = function
   | None -> message (Sys.getcwd())
-  | Some s ->
+  | Some path ->
       begin
-	try Sys.chdir (System.glob s)
+	try Sys.chdir (System.expand_path_macros path)
 	with Sys_error str -> warning ("Cd failed: " ^ str)
       end;
       if_verbose message (Sys.getcwd())