Add support for XDG_DATA_HOME and XDG_DATA_DIRS.

From Tom Prince

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

2 files changed, 20 insertions, 5 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index 0991fb7a12..5cffad06c8 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -51,11 +51,26 @@ let path_to_list p =
   let sep = if Sys.os_type = "Win32" then ';' else ':' in
     Util.split_string_at sep p
 
-let coqpath () =
+let xdg_data_home =
+  Filename.concat
+    (System.getenv_else "XDG_DATA_HOME" (Filename.concat System.home ".local/share"))
+    "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" ]
+
+let xdg_dirs =
+  let dirs = xdg_data_home :: xdg_data_dirs
+  in
+  List.rev (List.filter Sys.file_exists dirs)
+
+let coqpath =
   try
     let path = Sys.getenv "COQPATH" in
-      List.rev (path_to_list path)
-  with _ -> []
+      List.rev (List.filter Sys.file_exists (path_to_list path))
+  with Not_found -> []
 
 let rec which l f =
   match l with
@@ -89,7 +104,6 @@ let camllib () =
     let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in
     Util.strip res
 
-(* TODO : essayer aussi camlbin *)
 let camlp4bin () =
   if !Flags.camlp4bin_spec then !Flags.camlp4bin else
     if !Flags.boot then Coq_config.camlp4bin else
diff --git a/lib/envars.mli b/lib/envars.mli
index 3f8ac5ecc2..d2799074eb 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -15,7 +15,8 @@ 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 coqpath : unit -> string list
+val xdg_dirs : string list
+val coqpath : string list
 
 val camlbin : unit -> string
 val camlp4bin : unit -> string