Revert copy/pasted function in to minilib thanks to clib.cma

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

11 files changed, 69 insertions, 45 deletions

diff --git a/lib/cUnix.mli b/lib/cUnix.mli
index 00419bc97..c740d1254 100644
--- a/lib/cUnix.mli
+++ b/lib/cUnix.mli
@@ -12,6 +12,11 @@ type physical_path = string
 type load_path = physical_path list
 
 val canonical_path_name : string -> string
+val remove_path_dot : string -> string
+val strip_path : string -> string
+(** correct_path f dir = dir/f if f is relative *)
+val correct_path : string -> string -> string
+
 
 val physical_path_of_string : string -> physical_path
 val string_of_physical_path : physical_path -> string
@@ -30,3 +35,6 @@ val file_readable_p : string -> bool
 val run_command : (string -> string) -> (string -> unit) -> string ->
   Unix.process_status * string
 
+(** checks if two file names refer to the same (existing) file *)
+val same_file : string -> string -> bool
+
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 65d3a1562..36059fad3 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -3,6 +3,7 @@ Segmenttree
 Unicodetable
 Util
 Serialize
+Xml_utils
 Flags
 CUnix
 Envars
diff --git a/lib/envars.ml b/lib/envars.ml
index c6bf8aee0..71525f055 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -20,6 +20,15 @@ let safe_getenv warning n = getenv_else n (fun () ->
 (* On win32, the home directory is probably not in $HOME, but in
    some other environment variable *)
 
+let (/) = Filename.concat
+
+let coqify d = d / "coq"
+
+let relative_base =
+  Filename.dirname (Filename.dirname Sys.executable_name)
+
+let opt2list = function None -> [] | Some x -> [x]
+
 let home ~warn =
   getenv_else "HOME" (fun () ->
     try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
@@ -96,25 +105,34 @@ let path_to_list p =
     Util.split_string_at sep p
 
 let xdg_data_home warning =
-  Filename.concat
-    (getenv_else "XDG_DATA_HOME" (fun () -> Filename.concat (home warning) ".local/share"))
-    "coq"
-
-let xdg_config_home ~warn =
-  Filename.concat
-    (getenv_else "XDG_CONFIG_HOME" (fun () -> Filename.concat (home ~warn) ".config"))
-    "coq"
-
-let xdg_data_dirs =
-  (try
-    List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
-  with Not_found -> ["/usr/local/share/coq";"/usr/share/coq"])
-    @ (match Coq_config.datadir with |None -> [] |Some datadir -> [datadir])
+  coqify
+    (getenv_else "XDG_DATA_HOME" (fun () -> (home warning) / ".local/share"))
+
+let xdg_config_home warn =
+  coqify
+    (getenv_else "XDG_CONFIG_HOME" (fun () -> (home ~warn) / ".config"))
+
+let xdg_data_dirs warn =
+  let sys_dirs =
+    (try
+    List.map coqify (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
+   with
+      | Not_found when Sys.os_type = "Win32" -> [relative_base / "share"]
+      | Not_found -> ["/usr/local/share/coq";"/usr/share/coq"])
+  in
+  xdg_data_home warn :: sys_dirs @ opt2list Coq_config.datadir
+
+let xdg_config_dirs warn =
+  let sys_dirs =
+    try List.map coqify (path_to_list (Sys.getenv "XDG_CONFIG_DIRS"))
+    with
+      | Not_found when Sys.os_type = "Win32" -> [relative_base / "config"]
+      | Not_found -> ["/etc/xdg/coq"]
+  in
+  xdg_config_home warn :: sys_dirs @ opt2list Coq_config.configdir
 
 let xdg_dirs ~warn =
-  let dirs = xdg_data_home warn :: xdg_data_dirs
-  in
-  List.rev (List.filter Sys.file_exists dirs)
+  List.filter Sys.file_exists (xdg_data_dirs warn)
 
 let coqpath =
   try
diff --git a/lib/envars.mli b/lib/envars.mli
index ff4cf4a56..e99fd8e03 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -18,7 +18,10 @@ val coqbin : string
 val coqroot : string
 (* coqpath is stored in reverse order, since that is the order it
  * gets added to the searc path *)
-val xdg_config_home : warn:(string -> unit) -> string
+val xdg_config_home : (string -> unit) -> string
+val xdg_data_home : (string -> unit) -> string
+val xdg_config_dirs : (string -> unit) -> string list
+val xdg_data_dirs : (string -> unit) -> string list
 val xdg_dirs : warn:(string -> unit) -> string list
 val coqpath : string list
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 2f41c772a..5b66f9364 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -97,17 +97,6 @@ let is_unsafe s = Stringset.mem s !unsafe_set
 
 (* Flags for external tools *)
 
-let subst_command_placeholder s t =
-  let buff = Buffer.create (String.length s + String.length t) in
-  let i = ref 0 in
-  while (!i < String.length s) do
-    if s.[!i] = '%' & !i+1 < String.length s & s.[!i+1] = 's'
-    then (Buffer.add_string buff t;incr i)
-    else Buffer.add_char buff s.[!i];
-    incr i
-  done;
-  Buffer.contents buff
-
 let browser_cmd_fmt =
  try
   let coq_netscape_remote_var = "COQREMOTEBROWSER" in
diff --git a/lib/flags.mli b/lib/flags.mli
index b96bd402d..c47996621 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -81,9 +81,6 @@ val browser_cmd_fmt : string
 
 val is_standard_doc_url : string -> bool
 
-(** Substitute %s in the first chain by the second chain *)
-val subst_command_placeholder : string -> string -> string
-
 (** Options for specifying where coq librairies reside *)
 val coqlib_spec : bool ref
 val coqlib : string ref
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 77fc4ab09..1cbf0c780 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,6 +1,5 @@
 Xml_lexer
 Xml_parser
-Xml_utils
 Pp_control
 Compat
 Pp
diff --git a/lib/util.ml b/lib/util.ml
index 85ff2cbc4..ddc88e83b 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -67,6 +67,12 @@ let strip s =
   let a = lstrip_rec 0 and b = rstrip_rec (n-1) in
   String.sub s a (b-a+1)
 
+let string_map f s =
+  let l = String.length s in
+  let r = String.create l in
+  for i= 0 to (l - 1) do r.[i] <- f (s.[i]) done;
+  r
+
 let drop_simple_quotes s =
   let n = String.length s in
   if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
@@ -125,6 +131,17 @@ let parse_loadpath s =
     invalid_arg "parse_loadpath: find an empty dir in loadpath";
   l
 
+let subst_command_placeholder s t =
+  let buff = Buffer.create (String.length s + String.length t) in
+  let i = ref 0 in
+  while (!i < String.length s) do
+    if s.[!i] = '%' & !i+1 < String.length s & s.[!i+1] = 's'
+    then (Buffer.add_string buff t;incr i)
+    else Buffer.add_char buff s.[!i];
+    incr i
+  done;
+  Buffer.contents buff
+
 module Stringset = Set.Make(struct type t = string let compare (x:t) (y:t) = compare x y end)
 
 module Stringmap = Map.Make(struct type t = string let compare (x:t) (y:t) = compare x y end)
diff --git a/lib/util.mli b/lib/util.mli
index d98551823..d1a3f4308 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -45,6 +45,7 @@ val next_utf8 : string -> int -> int * int
 val explode : string -> string list
 val implode : string list -> string
 val strip : string -> string
+val string_map : (char -> char) -> string -> string
 val drop_simple_quotes : string -> string
 val string_index_from : string -> int -> string -> int
 val string_string_contains : where:string -> what:string -> bool
@@ -52,6 +53,8 @@ val plural : int -> string -> string
 val ordinal : int -> string
 val split_string_at : char -> string -> string list
 
+(** Substitute %s in the first chain by the second chain *)
+val subst_command_placeholder : string -> string -> string
 val parse_loadpath : string -> string list
 
 module Stringset : Set.S with type elt = string
diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml
index 1d09b1723..48ee546ca 100644
--- a/lib/xml_utils.ml
+++ b/lib/xml_utils.ml
@@ -24,17 +24,6 @@ exception Not_element of xml
 exception Not_pcdata of xml
 exception No_attribute of string
 
-let default_parser = Xml_parser.make()
-
-let parse (p:Xml_parser.t) (source:Xml_parser.source) =
-	(* local cast Xml.xml -> xml *)
-	(Obj.magic Xml_parser.parse p source : xml)
-
-let parse_in ch = parse default_parser (Xml_parser.SChannel ch)
-let parse_string str = parse default_parser (Xml_parser.SString str)
-
-let parse_file f = parse default_parser (Xml_parser.SFile f)
-
 let tag = function
 	| Element (tag,_,_) -> tag
 	| x -> raise (Not_element x)
diff --git a/lib/xml_utils.mli b/lib/xml_utils.mli
index 4a4a1309b..56e7f8076 100644
--- a/lib/xml_utils.mli
+++ b/lib/xml_utils.mli
@@ -29,7 +29,7 @@
   {i (c)Copyright 2002-2003 Nicolas Cannasse}
 *)
 
-open Xml_parser
+open Serialize
 
 (** {6 Xml Functions} *)