Fixed access to environment variables in CoqIDE. Up to now, those

variables where set at compile time...

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

7 files changed, 77 insertions, 47 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index a67d42202..dc285a103 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1603,6 +1603,7 @@ let forbid_quit_to_save () =
 
 let main files =
 
+  let data_dirs = Minilib.xdg_data_dirs () in
   (* Main window *)
   let w = GWindow.window
     ~wm_class:"CoqIde" ~wm_name:"CoqIde"
@@ -1613,11 +1614,14 @@ let main files =
   (try
      let icon_image = Filename.concat (List.find
        (fun x -> Sys.file_exists (Filename.concat x "coq.png"))
-       Minilib.xdg_data_dirs) "coq.png" in
+       data_dirs) "coq.png" in
      let icon = GdkPixbuf.from_file icon_image in
      w#set_icon (Some icon)
    with _ -> ());
 
+  let () = style_manager#set_search_path (data_dirs @ style_manager#search_path) in
+  let () = lang_manager#set_search_path (data_dirs @ lang_manager#search_path) in
+
   let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
 
   let new_f _ =
@@ -2252,7 +2256,7 @@ let main files =
     (fun () -> if current.show_toolbar then toolbar#misc#show () else toolbar#misc#hide ());
   refresh_style_hook :=
     (fun () ->
-      let style =  style_manager#style_scheme current.source_style in
+      let style = style_manager#style_scheme current.source_style in
       let iter_page p = p.script#source_buffer#set_style_scheme style in
       List.iter iter_page session_notebook#pages;
     );
@@ -2332,7 +2336,7 @@ let main files =
     (try
        let image = Filename.concat (List.find
 	 (fun x -> Sys.file_exists (Filename.concat x "coq.png"))
-	 Minilib.xdg_data_dirs) "coq.png" in
+	 data_dirs) "coq.png" in
        let startup_image = GdkPixbuf.from_file image in
        b#insert ~iter:b#start_iter "\n\n";
        b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image;
@@ -2344,7 +2348,7 @@ let main files =
     (try
        let image = Filename.concat (List.find
 	 (fun x -> Sys.file_exists (Filename.concat x "coq.png"))
-	 Minilib.xdg_data_dirs) "coq.png" in
+	 data_dirs) "coq.png" in
        let startup_image = GdkPixbuf.from_file image in
        b#insert ~iter:b#start_iter "\n\n";
        b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image;
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 2507c914a..9350c765c 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -316,7 +316,7 @@ let url_for_keyword =
 	let cin =
 	  try let index_urls = Filename.concat (List.find
             (fun x -> Sys.file_exists (Filename.concat x "index_urls.txt"))
-	    Minilib.xdg_config_dirs) "index_urls.txt" in
+	    (Minilib.xdg_config_dirs ())) "index_urls.txt" in
 	    open_in index_urls
 	  with Not_found ->
 	    let doc_url = doc_url () in
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 2400872a4..eba5499e9 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -71,33 +71,54 @@ let path_to_list p =
 (* On win32, the home directory is probably not in $HOME, but in
    some other environment variable *)
 
-let home =
+let home () =
   try Sys.getenv "HOME" with Not_found ->
     try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
       try Sys.getenv "USERPROFILE" with Not_found -> Filename.current_dir_name
 
-let xdg_config_home =
+let xdg_config_home () =
   try
     Filename.concat (Sys.getenv "XDG_CONFIG_HOME") "coq"
   with Not_found ->
-    Filename.concat home "/.config/coq"
-
-let xdg_config_dirs =
-  xdg_config_home :: (try
-    List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_CONFIG_DIRS"))
-  with Not_found -> ["/etc/xdg/coq"])@(match Coq_config.configdir with |None -> [] |Some d -> [d])
+    let home_dir = home () in
+    Filename.concat home_dir "/.config/coq"
+
+let xdg_config_dirs () =
+  let config_home = xdg_config_home () in
+  let config_list =
+    try path_to_list (Sys.getenv "XDG_CONFIG_DIRS")
+    with Not_found -> ["/etc/xdg"]
+  in
+  let remaining =
+    List.map (fun dir -> Filename.concat dir "coq") config_list
+  in
+  let def = match Coq_config.configdir with
+  | None -> []
+  | Some d -> [d]
+  in
+  config_home :: remaining @ def
 
-let xdg_data_home =
+let xdg_data_home () =
   try
     Filename.concat (Sys.getenv "XDG_DATA_HOME") "coq"
   with Not_found ->
-    Filename.concat home "/.local/share/coq"
-
-let xdg_data_dirs =
-  xdg_data_home :: (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 d -> [d])
+    let home_dir = home () in
+    Filename.concat home_dir "/.local/share/coq"
+
+let xdg_data_dirs () =
+  let data_home = xdg_data_home () in
+  let data_list =
+    try path_to_list (Sys.getenv "XDG_DATA_DIRS")
+    with Not_found -> ["/usr/local/share";"/usr/share"]
+  in
+  let remaining =
+    List.map (fun dir -> Filename.concat dir "coq") data_list
+  in
+  let def = match Coq_config.datadir with
+  | None -> []
+  | Some d -> [d]
+  in
+  data_home :: remaining @ def
 
 let coqtop_path = ref ""
 
diff --git a/ide/minilib.mli b/ide/minilib.mli
index 53d6c87c2..7df949cbb 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -21,11 +21,11 @@ val string_map : (char -> char) -> string -> string
 
 val subst_command_placeholder : string -> string -> string
 
-val home : string
-val xdg_config_home : string
-val xdg_config_dirs : string list
-val xdg_data_home : string
-val xdg_data_dirs : string list
+val home : unit -> string
+val xdg_config_home : unit -> string
+val xdg_config_dirs : unit -> string list
+val xdg_data_home : unit -> string
+val xdg_data_dirs : unit -> string list
 
 val coqtop_path : string ref
 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 6e18b4d34..9c0a91e65 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -9,29 +9,15 @@
 open Configwin
 open Printf
 
-let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc"
-let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys"
 let lang_manager = GSourceView2.source_language_manager ~default:true
-let () = lang_manager#set_search_path
-  (Minilib.xdg_data_dirs@lang_manager#search_path)
 let style_manager = GSourceView2.source_style_scheme_manager ~default:true
-let () = style_manager#set_search_path
-  (Minilib.xdg_data_dirs@style_manager#search_path)
 
 let get_config_file name =
+  let config_dirs = Minilib.xdg_config_dirs () in
   let find_config dir = Sys.file_exists (Filename.concat dir name) in
-  let config_dir = List.find find_config Minilib.xdg_config_dirs in
+  let config_dir = List.find find_config config_dirs in
   Filename.concat config_dir name
 
-(* Small hack to handle v8.3 to v8.4 change in configuration file *)
-let loaded_pref_file =
-  try get_config_file "coqiderc"
-  with Not_found -> Filename.concat Minilib.home ".coqiderc"
-
-let loaded_accel_file =
-  try get_config_file "coqide.keys"
-  with Not_found -> Filename.concat Minilib.home ".coqide.keys"
-
 let mod_to_str (m:Gdk.Tags.modifier) =
   match m with
     | `MOD1 -> "<Alt>"
@@ -221,8 +207,11 @@ let current = {
   }
 
 let save_pref () =
-  if not (Sys.file_exists Minilib.xdg_config_home)
-  then Unix.mkdir Minilib.xdg_config_home 0o700;
+  let home = Minilib.xdg_config_home () in
+  let pref_file = Filename.concat home "coqiderc" in
+  let accel_file = Filename.concat home "coqide.keys" in
+  if not (Sys.file_exists home)
+  then Unix.mkdir home 0o700;
   let () = try GtkData.AccelMap.save accel_file with _ -> () in
   let p = current in
 
@@ -285,6 +274,22 @@ let save_pref () =
     Config_lexer.print_file pref_file
 
 let load_pref () =
+
+  (* Small hack to handle v8.3 to v8.4 change in configuration file *)
+  let loaded_pref_file =
+    try get_config_file "coqiderc"
+    with Not_found ->
+      let home = Minilib.home () in
+      Filename.concat home ".coqiderc"
+  in
+
+  let loaded_accel_file =
+    try get_config_file "coqide.keys"
+    with Not_found ->
+      let home = Minilib.home () in
+      Filename.concat home ".coqide.keys"
+  in
+
   let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in
 
     let m = Config_lexer.load_file loaded_pref_file in
@@ -621,6 +626,7 @@ let configure ?(apply=(fun () -> ())) () =
       current.source_style <- s;
       !refresh_style_hook ()
     in
+    let () = style_manager#force_rescan () in
     combo "Highlighting style:"
       ~f ~new_allowed:false
       style_manager#style_scheme_ids current.source_style
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 7dbd04529..8a3f41581 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -35,7 +35,6 @@ class type widget =
     method apply : unit -> unit
   end
 
-let file_html_config = Filename.concat Configwin_messages.home ".configwin_html"
 
 let debug = false
 let dbg = if debug then prerr_endline else (fun _ -> ())
@@ -43,6 +42,8 @@ let dbg = if debug then prerr_endline else (fun _ -> ())
 (** Return the config group for the html config file,
    and the option for bindings. *)
 let html_config_file_and_option () =
+  let home = Minilib.home () in
+  let file_html_config = Filename.concat home ".configwin_html" in
   let ini = new O.group in
   let bindings = new O.list_cp
       Configwin_types.htmlbinding_cp_wrapper
diff --git a/ide/utils/configwin_messages.ml b/ide/utils/configwin_messages.ml
index de2924318..9818a0f3f 100644
--- a/ide/utils/configwin_messages.ml
+++ b/ide/utils/configwin_messages.ml
@@ -30,8 +30,6 @@ let version = "1.2";;
 
 let html_config = "Configwin bindings configurator for html parameters"
 
-let home = Minilib.home
-
 let mCapture = "Capture";;
 let mType_key = "Type key" ;;
 let mAdd = "Add";;