CoqIdE configuration file won't pollute your home anymore

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

8 files changed, 42 insertions, 33 deletions

diff --git a/CHANGES b/CHANGES
index 2521e6c75..dd65cba39 100644
--- a/CHANGES
+++ b/CHANGES
@@ -191,11 +191,14 @@ CoqIDE
 
 - Coqide now runs coqtop as separated process, making it more robust:
   coqtop subprocess can be interrupted, or even killed and relaunched
-  (cf button "Restart Coq", ex-"Go to Start"). For allowing such interrupts,
-  the Windows version of coqide now requires Windows >= XP SP1.
+  (cf button "Restart Coq", ex-"Go to Start"). For allowing such
+  interrupts, the Windows version of coqide now requires Windows >= XP
+  SP1.
 - The Coqide parsing of sentences has be reworked and now supports
   tactic delimitation via { }.
 - Coqide now accepts the Abort command (wish #2357).
+- Preference files have moved to $XDG_CONFIG_HOME/coq and accelerators
+  are not stored in a list anymore.
 
 Tools
 
@@ -208,7 +211,7 @@ Tools
   * More variables are given by coqtop -config, others are defined only if the
     users doesn't have defined them elsewhere. Consequently, generated makefile
     should work directly on any architecture.
-  * Packager can take advantage of $(DSTROOT) introduction
+  * Packagers can take advantage of $(DSTROOT) introduction
 
 Changes from V8.2 to V8.3
 =========================
diff --git a/INSTALL.ide b/INSTALL.ide
index d09df2eb0..300d17b19 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -23,10 +23,10 @@ On Gentoo GNU/Linux, do:
 Else, read the rest of this document to compile your own CoqIde.
 
 REQUIREMENT:
-	- OCaml >= 3.10 with native threads support.
+	- OCaml >= 3.11 with native threads support.
 	- make world must succeed.
 	- The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
-	  The official supported version is at least 2.8.x.
+	  The official supported version is at least 2.10.x.
 	  You may still compile CoqIde with older versions and 
           use all features.
 	  Run 
@@ -42,7 +42,7 @@ REQUIREMENT:
 
         - The OCaml bindings for GTK+ 2.x, lablgtk2.
 
-	  You need at least version 2.10.0.
+	  You need at least version 2.12.0.
 
 	  Your distribution may contain precompiled packages. For
           example, for Debian, run
@@ -104,17 +104,14 @@ INSTALLATION
 
 
 NOTES
-There are three configuration files located in your $(HOME) dir. 
+There are three configuration files located in your $(XDG_CONFIG_HOME)/coq dir.
  You may need to set HOME to some sensible value under Windows.
 
-- .coqiderc is generated by coqide itself. It may be edited by hand or 
+- coqiderc is generated by coqide itself. It may be edited by hand or 
   by using the Preference menu from coqide. It will be generated the first time
   you save your the preferences in Coqide.
 
-- .coqide-gtk2rc is a standard Gtk2 configuration file. A sample file can be
-  found in the coq lib "ide" subdir.
-
-- .coqide.keys is a standard Gtk2 accelerator dump. You may edit this file 
+- coqide.keys is a standard Gtk2 accelerator dump. You may edit this file 
   to change the default shortcuts for the menus.
 
 Read ide/FAQ for more informations.
@@ -127,8 +124,8 @@ TROUBLESHOOTING
     Some users may experiment problems with unwanted automatic
     templates while using Coqide. This is due to a change in the
     modifiers keys available through GTK. The straightest way to get
-    rid of the problem is to edit by hand your .coqiderc (either
-    /home/<user>/.coqiderc under Linux, or 
-    C:\Documents and Settings\<user>\.coqiderc under Windows) 
+    rid of the problem is to edit by hand your coqiderc (either
+    /home/<user>/.config/coq/coqiderc under Linux, or 
+    C:\Documents and Settings\<user>\.config\coq\coqiderc under Windows) 
     and replace any occurence of MOD4 by MOD1.
 
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index eddbb8d64..88892ff31 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -2347,8 +2347,8 @@ Depending on your configuration, use either one of these two methods
 \begin{itemize}
 
 \item Insert \texttt{gtk-key-theme-name = "Emacs"}
-    in your \texttt{.coqide-gtk2rc} file. It may be in the current dir
-    or in \verb#$HOME# dir. This is done by default.
+    in your \texttt{coqide-gtk2rc} file. It should be in
+    \verb#$XDG_CONFIG_DIRS/coq# dir. This is done by default.
 
 \item If in Gnome, run the gnome configuration editor (\texttt{gconf-editor})
 and set key \texttt{gtk-key-theme} to \texttt{Emacs} in the category
@@ -2416,7 +2416,7 @@ xmodmap -e "keycode  26 = e E F14 F14"
 \verb=bind "F13" {"insert-at-cursor" ("=$\forall$\verb=")}=\\
 \verb=bind "F14" {"insert-at-cursor" ("=$\exists$\verb=")}=
 
-	to your "binding "text"" section in \verb#.coqiderc-gtk2rc.#
+	to your "binding "text"" section in \verb#coqiderc-gtk2rc#.
 	The last arguments to {\tt bind} between "" are
         the UTF-8 encodings for 0x2200 and 0x2203.
 	You can compute these encodings using the lablgtk2 toplevel with
@@ -2430,8 +2430,8 @@ Glib.Utf8.from_unichar 0x2200;;
 \Question{How to customize the shortcuts for menus?}
  Two solutions are offered:
 \begin{itemize}
-\item Edit \$HOME/.coqide.keys by hand or
-\item Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then
+\item Edit \$XDG_CONFIG_HOME/coq/coqide.keys (\$HOME/.config/coq/coqide.keys) by hand or
+\item Add "gtk-can-change-accels = 1" in your coqide-gtk2rc file. Then
     from \CoqIde, you may select a menu entry and press the desired 
     shortcut. 
 \end{itemize}
@@ -2451,9 +2451,9 @@ Glib.Utf8.from_unichar 0x2200;;
 Some users may experiment problems with unwanted automatic
 templates while using Coqide. This is due to a change in the
 modifiers keys available through GTK. The straightest way to get
-rid of the problem is to edit by hand your .coqiderc (either
-\verb|/home/<user>/.coqiderc| under Linux, or \\
-\verb|C:\Documents and Settings\<user>\.coqiderc| under Windows) 
+rid of the problem is to edit by hand your coqiderc (either
+\verb|/home/<user>/.config/coq/coqiderc| under Linux, or \\
+\verb|C:\Documents and Settings\<user>\.config\coq\coqiderc| under Windows) 
     and replace any occurence of \texttt{MOD4} by \texttt{MOD1}.
 
 
diff --git a/ide/FAQ b/ide/FAQ
index 39dc095e4..f07f229fc 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -6,8 +6,8 @@ R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more i
 Q1) How to enable Emacs keybindings?
 R1: Insert 
 	gtk-key-theme-name = "Emacs"
-    in your ".coqide-gtk2rc" file. It may be in the current dir
-    or in $HOME dir. This is done by default.
+    in your "coqide-gtk2rc" file. It should be in $XDG_CONFIG_DIRS/coq dir.
+    This is done by default.
 
 Q2) How to enable antialiased fonts?
 R2) Set the GDK_USE_XFT variable to 1. This is by default with Gtk >= 2.2.
@@ -41,7 +41,7 @@ R5)-First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script
 	and then to add   
 		bind "F13" {"insert-at-cursor" ("∀")}
 		bind "F14" {"insert-at-cursor" ("∃")}
-	to your "binding "text"" section in .coqiderc-gtk2rc.
+	to your "binding "text"" section in coqiderc-gtk2rc.
 	The strange ("∀") argument is the UTF-8 encoding for
 	0x2200. 
 	You can compute these encodings using the lablgtk2 toplevel with 
@@ -51,8 +51,8 @@ R5)-First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script
 
 Q6) How to customize the shortcuts for menus?
 R6) Two solutions are offered:
-  - Edit $HOME/.coqide.keys by hand or
-  - Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then
+  - Edit $XDG_CONFIG_HOME/coq/coqide.keys by hand or
+  - Add "gtk-can-change-accels = 1" in your coqide-gtk2rc file. Then
     from CoqIde, you may select a menu entry and press the desired 
     shortcut. 
 
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 933baa5dc..57699c686 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -25,7 +25,7 @@ rule prefs m = parse
   |ignore* (ident as id) ignore* '=' { let conf = str_list [] lexbuf in
 				 prefs (Stringmap.add id conf m) lexbuf }
   | _     { let c = lexeme_start lexbuf in
-	      eprintf ".coqiderc: invalid character (%d)\n@." c;
+	      eprintf "coqiderc: invalid character (%d)\n@." c;
 	      prefs m lexbuf }
   | eof   { m }
 
@@ -41,7 +41,7 @@ and string = parse
   | '"'  { Buffer.add_char string_buffer '"' }
   | '\\' '"' | _
          { Buffer.add_string string_buffer (lexeme lexbuf); string lexbuf }
-  | eof  { eprintf ".coqiderc: unterminated string\n@." }
+  | eof  { eprintf "coqiderc: unterminated string\n@." }
 
 {
 
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 54be52c19..65ff4378e 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -70,7 +70,13 @@ let subst_command_placeholder s t =
 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 -> "."
+      try Sys.getenv "USERPROFILE" with Not_found -> Filename.current_dir_name
+
+let xdg_config_home =
+  try
+    Filename.concat (Sys.getenv "XDG_CONFIG_HOME") "coq"
+  with Not_found ->
+    Filename.concat home "/.config/coq"
 
 let coqlib = ref ""
 let coqtop_path = ref ""
diff --git a/ide/minilib.mli b/ide/minilib.mli
index 44e570301..749180756 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -22,6 +22,7 @@ val string_map : (char -> char) -> string -> string
 val subst_command_placeholder : string -> string -> string
 
 val home : string
+val xdg_config_home : string
 
 val coqlib : string ref
 val coqtop_path : string ref
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 3f2c69acd..14608f984 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -10,9 +10,9 @@
 open Configwin
 open Printf
 
-let pref_file = Filename.concat Minilib.home ".coqiderc"
+let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc"
 
-let accel_file = Filename.concat Minilib.home ".coqide.keys"
+let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys"
 
 let mod_to_str (m:Gdk.Tags.modifier) =
   match m with
@@ -168,6 +168,8 @@ let contextual_menus_on_goal = ref (fun x -> ())
 let resize_window = ref (fun () -> ())
 
 let save_pref () =
+  if not (Sys.file_exists Minilib.xdg_config_home)
+  then Unix.mkdir Minilib.xdg_config_home 0o700;
   (try GtkData.AccelMap.save accel_file
   with _ -> ());
   let p = !current in