1 files changed, 266 insertions, 171 deletions

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 790bf560..2fb5023f 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -1,56 +1,88 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: preferences.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Configwin
 open Printf
-open Util
 
-let pref_file = Filename.concat System.home ".coqiderc"
+let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc"
+let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys"
+
+let get_config_file name =
+  let find_config dir = Sys.file_exists (Filename.concat dir name) in
+  let config_dir = List.find find_config Minilib.xdg_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 accel_file = Filename.concat System.home ".coqide.keys"
+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 -> "MOD1"
-    | `MOD2 -> "MOD2"
-    | `MOD3 -> "MOD3"
-    | `MOD4 -> "MOD4"
-    | `MOD5 -> "MOD5"
-    | `BUTTON1 -> "BUTTON1"
-    | `BUTTON2 -> "BUTTON2"
-    | `BUTTON3 -> "BUTTON3"
-    | `BUTTON4 -> "BUTTON4"
-    | `BUTTON5 -> "BUTTON5"
-    | `CONTROL -> "CONTROL"
-    | `LOCK -> "LOCK"
-    | `SHIFT -> "SHIFT"
-
-let (str_to_mod:string -> Gdk.Tags.modifier) =
-  function
-    | "MOD1" -> `MOD1
-    | "MOD2" -> `MOD2
-    | "MOD3" -> `MOD3
-    | "MOD4" -> `MOD4
-    | "MOD5" -> `MOD5
-    | "BUTTON1" -> `BUTTON1
-    | "BUTTON2" -> `BUTTON2
-    | "BUTTON3" -> `BUTTON3
-    | "BUTTON4" -> `BUTTON4
-    | "BUTTON5" -> `BUTTON5
-    | "CONTROL" -> `CONTROL
-    | "LOCK" -> `LOCK
-    | "SHIFT" -> `SHIFT
-    | s -> `MOD1
+    | `MOD1 -> "<Alt>"
+    | `MOD2 -> "<Mod2>"
+    | `MOD3 -> "<Mod3>"
+    | `MOD4 -> "<Mod4>"
+    | `MOD5 -> "<Mod5>"
+    | `CONTROL -> "<Control>"
+    | `SHIFT -> "<Shift>"
+    | `HYPER -> "<Hyper>"
+    | `META -> "<Meta>"
+    | `RELEASE -> ""
+    | `SUPER -> "<Super>"
+    |  `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> ""
+
+let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l
+
+let str_to_mod_list s = snd (GtkData.AccelGroup.parse s)
+
+type project_behavior = Ignore_args | Append_args | Subst_args
+
+let string_of_project_behavior = function
+  |Ignore_args -> "ignored"
+  |Append_args -> "appended to arguments"
+  |Subst_args -> "taken instead of arguments"
+
+let project_behavior_of_string s =
+  if s = "taken instead of arguments" then Subst_args
+  else if s = "appended to arguments" then Append_args
+  else Ignore_args
+
+type inputenc = Elocale | Eutf8 | Emanual of string
+
+let string_of_inputenc = function
+  |Elocale -> "LOCALE"
+  |Eutf8 -> "UTF-8"
+  |Emanual s -> s
+
+let inputenc_of_string s =
+      (if s = "UTF-8" then Eutf8
+       else if s = "LOCALE" then Elocale
+       else Emanual s)
+
+
+(** Hooks *)
+
+let refresh_font_hook = ref (fun () -> ())
+let refresh_background_color_hook = ref (fun () -> ())
+let refresh_toolbar_hook = ref (fun () -> ())
+let auto_complete_hook = ref (fun x -> ())
+let contextual_menus_on_goal_hook = ref (fun x -> ())
+let resize_window_hook = ref (fun () -> ())
+let refresh_tabs_hook = ref (fun () -> ())
 
 type pref =
     {
+      mutable cmd_coqtop : string option;
       mutable cmd_coqc : string;
       mutable cmd_make : string;
       mutable cmd_coqmakefile : string;
@@ -63,18 +95,19 @@ type pref =
       mutable auto_save_delay : int;
       mutable auto_save_name : string * string;
 
-      mutable encoding_use_locale : bool;
-      mutable encoding_use_utf8 : bool;
-      mutable encoding_manual : string;
+      mutable read_project : project_behavior;
+      mutable project_file_name : string;
+
+      mutable encoding : inputenc;
 
       mutable automatic_tactics : string list;
       mutable cmd_print : string;
 
-      mutable modifier_for_navigation : Gdk.Tags.modifier list;
-      mutable modifier_for_templates : Gdk.Tags.modifier list;
-      mutable modifier_for_tactics : Gdk.Tags.modifier list;
-      mutable modifier_for_display : Gdk.Tags.modifier list;
-      mutable modifiers_valid : Gdk.Tags.modifier list;
+      mutable modifier_for_navigation : string;
+      mutable modifier_for_templates : string;
+      mutable modifier_for_tactics : string;
+      mutable modifier_for_display : string;
+      mutable modifiers_valid : string;
 
       mutable cmd_browse : string;
       mutable cmd_editor : string;
@@ -95,15 +128,20 @@ type pref =
 *)
       mutable auto_complete : bool;
       mutable stop_before : bool;
-      mutable lax_syntax : bool;
       mutable vertical_tabs : bool;
       mutable opposite_tabs : bool;
+
+      mutable background_color : string;
+      mutable processing_color : string;
+      mutable processed_color : string;
+
 }
 
 let use_default_doc_url = "(automatic)"
 
 let (current:pref ref) =
   ref {
+    cmd_coqtop = None;
     cmd_coqc = "coqc";
     cmd_make = "make";
     cmd_coqmakefile = "coq_makefile -o makefile *.v";
@@ -117,25 +155,28 @@ let (current:pref ref) =
     auto_save_delay = 10000;
     auto_save_name = "#","#";
 
-    encoding_use_locale = true;
-    encoding_use_utf8 = false;
-    encoding_manual = "ISO_8859-1";
+    read_project = Ignore_args;
+    project_file_name = "_CoqProject";
+
+    encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale;
 
     automatic_tactics = ["trivial"; "tauto"; "auto"; "omega";
 			 "auto with *"; "intuition" ];
 
-    modifier_for_navigation = [`CONTROL; `MOD1];
-    modifier_for_templates = [`CONTROL; `SHIFT];
-    modifier_for_tactics = [`CONTROL; `MOD1];
-    modifier_for_display = [`MOD1;`SHIFT];
-    modifiers_valid = [`SHIFT; `CONTROL; `MOD1];
+    modifier_for_navigation = "<Control><Alt>";
+    modifier_for_templates = "<Control><Shift>";
+    modifier_for_tactics = "<Control><Alt>";
+    modifier_for_display = "<Alt><Shift>";
+    modifiers_valid = "<Alt><Control><Shift>";
 
 
     cmd_browse = Flags.browser_cmd_fmt;
     cmd_editor = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s";
 
 (*    text_font = Pango.Font.from_string "sans 12";*)
-    text_font = Pango.Font.from_string "Monospace 10";
+    text_font = Pango.Font.from_string (match Coq_config.gtk_platform with
+					  |`QUARTZ -> "Arial Unicode MS 11"
+					  |_ -> "Monospace 10");
 
     doc_url = Coq_config.wwwrefman;
     library_url = Coq_config.wwwstdlib;
@@ -151,30 +192,25 @@ let (current:pref ref) =
 *)
     auto_complete = false;
     stop_before = true;
-    lax_syntax = true;
     vertical_tabs = false;
     opposite_tabs = false;
-  }
-
-
-let change_font = ref (fun f -> ())
 
-let show_toolbar = ref (fun x -> ())
+    background_color = "cornsilk";
+    processed_color = "light green";
+    processing_color = "light blue";
 
-let auto_complete = ref (fun x -> ())
-
-let contextual_menus_on_goal = ref (fun x -> ())
-
-let resize_window = ref (fun () -> ())
+  }
 
 let save_pref () =
-  (try GtkData.AccelMap.save accel_file
-  with _ -> ());
+  if not (Sys.file_exists Minilib.xdg_config_home)
+  then Unix.mkdir Minilib.xdg_config_home 0o700;
+  let () = try GtkData.AccelMap.save accel_file with _ -> () in
   let p = !current in
-  try
-    let add = Stringmap.add in
+
+    let add = Minilib.Stringmap.add in
     let (++) x f = f x in
-    Stringmap.empty ++
+    Minilib.Stringmap.empty ++
+    add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++
     add "cmd_coqc" [p.cmd_coqc] ++
     add "cmd_make" [p.cmd_make] ++
     add "cmd_coqmakefile" [p.cmd_coqmakefile] ++
@@ -186,22 +222,18 @@ let save_pref () =
     add "auto_save_delay" [string_of_int p.auto_save_delay] ++
     add "auto_save_name" [fst p.auto_save_name; snd p.auto_save_name] ++
 
-    add "encoding_use_locale" [string_of_bool p.encoding_use_locale] ++
-    add "encoding_use_utf8" [string_of_bool p.encoding_use_utf8] ++
-    add "encoding_manual" [p.encoding_manual] ++
+    add "project_options" [string_of_project_behavior p.read_project] ++
+    add "project_file_name" [p.project_file_name] ++
+
+    add "encoding" [string_of_inputenc p.encoding] ++
 
     add "automatic_tactics" p.automatic_tactics ++
     add "cmd_print" [p.cmd_print] ++
-    add "modifier_for_navigation"
-      (List.map mod_to_str p.modifier_for_navigation) ++
-    add "modifier_for_templates"
-      (List.map mod_to_str p.modifier_for_templates) ++
-    add "modifier_for_tactics"
-      (List.map mod_to_str p.modifier_for_tactics) ++
-    add "modifier_for_display"
-      (List.map mod_to_str p.modifier_for_display) ++
-    add "modifiers_valid"
-      (List.map mod_to_str p.modifiers_valid) ++
+    add "modifier_for_navigation" [p.modifier_for_navigation] ++
+    add "modifier_for_templates" [p.modifier_for_templates] ++
+    add "modifier_for_tactics" [p.modifier_for_tactics] ++
+    add "modifier_for_display" [p.modifier_for_display] ++
+    add "modifiers_valid" [p.modifiers_valid] ++
     add "cmd_browse" [p.cmd_browse] ++
     add "cmd_editor" [p.cmd_editor] ++
 
@@ -218,19 +250,20 @@ let save_pref () =
     add "query_window_width" [string_of_int p.query_window_width] ++
     add "auto_complete" [string_of_bool p.auto_complete] ++
     add "stop_before" [string_of_bool p.stop_before] ++
-    add "lax_syntax" [string_of_bool p.lax_syntax] ++
     add "vertical_tabs" [string_of_bool p.vertical_tabs] ++
     add "opposite_tabs" [string_of_bool p.opposite_tabs] ++
+    add "background_color" [p.background_color] ++
+    add "processing_color" [p.processing_color] ++
+    add "processed_color" [p.processed_color] ++
     Config_lexer.print_file pref_file
-  with _ -> prerr_endline "Could not save preferences."
 
 let load_pref () =
-  (try GtkData.AccelMap.load accel_file with _ -> ());
+  let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in
   let p = !current in
-  try
-    let m = Config_lexer.load_file pref_file in
+
+    let m = Config_lexer.load_file loaded_pref_file in
     let np = { p with cmd_coqc = p.cmd_coqc } in
-    let set k f = try let v = Stringmap.find k m in f v with _ -> () in
+    let set k f = try let v = Minilib.Stringmap.find k m in f v with _ -> () in
     let set_hd k f = set k (fun v -> f (List.hd v)) in
     let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in
     let set_int k f = set_hd k (fun v -> f (int_of_string v)) in
@@ -238,6 +271,8 @@ let load_pref () =
     let set_command_with_pair_compat k f =
       set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit)
     in
+    let set_option k f = set k (fun v -> f (match v with |[] -> None |h::_ ->  Some h)) in
+    set_option "cmd_coqtop" (fun v -> np.cmd_coqtop <- v);
     set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v);
     set_hd "cmd_make" (fun v -> np.cmd_make <- v);
     set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v);
@@ -248,22 +283,23 @@ let load_pref () =
     set_bool "auto_save" (fun v -> np.auto_save <- v);
     set_int "auto_save_delay" (fun v -> np.auto_save_delay <- v);
     set_pair "auto_save_name" (fun v1 v2 -> np.auto_save_name <- (v1,v2));
-    set_bool "encoding_use_locale" (fun v -> np.encoding_use_locale <- v);
-    set_bool "encoding_use_utf8" (fun v -> np.encoding_use_utf8 <- v);
-    set_hd "encoding_manual" (fun v -> np.encoding_manual <- v);
+    set_hd "encoding" (fun v -> np.encoding <- (inputenc_of_string v));
+    set_hd "project_options"
+      (fun v -> np.read_project <- (project_behavior_of_string v));
+    set_hd "project_file_name" (fun v -> np.project_file_name <- v);
     set "automatic_tactics"
       (fun v -> np.automatic_tactics <- v);
     set_hd "cmd_print" (fun v -> np.cmd_print <- v);
-    set "modifier_for_navigation"
-      (fun v -> np.modifier_for_navigation <- List.map str_to_mod v);
-    set "modifier_for_templates"
-      (fun v -> np.modifier_for_templates <- List.map str_to_mod v);
-    set "modifier_for_tactics"
-      (fun v -> np.modifier_for_tactics <- List.map str_to_mod v);
-    set "modifier_for_display"
-      (fun v -> np.modifier_for_display <- List.map str_to_mod v);
-    set "modifiers_valid"
-      (fun v -> np.modifiers_valid <- List.map str_to_mod v);
+    set_hd "modifier_for_navigation"
+      (fun v -> np.modifier_for_navigation <- v);
+    set_hd "modifier_for_templates"
+      (fun v -> np.modifier_for_templates <- v);
+    set_hd "modifier_for_tactics"
+      (fun v -> np.modifier_for_tactics <- v);
+    set_hd "modifier_for_display"
+      (fun v -> np.modifier_for_display <- v);
+    set_hd "modifiers_valid"
+      (fun v -> np.modifiers_valid <- v);
     set_command_with_pair_compat "cmd_browse" (fun v -> np.cmd_browse <- v);
     set_command_with_pair_compat "cmd_editor" (fun v -> np.cmd_editor <- v);
     set_hd "text_font" (fun v -> np.text_font <- Pango.Font.from_string v);
@@ -274,7 +310,7 @@ let load_pref () =
         v <> Coq_config.wwwcoq ^ "doc" &&
 	v <> Coq_config.wwwcoq ^ "doc/"
       then
-	prerr_endline ("Warning: Non-standard URL for Coq documentation in preference file: "^v);
+	(*prerr_endline ("Warning: Non-standard URL for Coq documentation in preference file: "^v);*)
       np.doc_url <- v);
     set_hd "library_url" (fun v -> np.library_url <- v);
     set_bool "show_toolbar" (fun v -> np.show_toolbar <- v);
@@ -286,26 +322,21 @@ let load_pref () =
     set_int "query_window_height" (fun v -> np.query_window_height <- v);
     set_bool "auto_complete" (fun v -> np.auto_complete <- v);
     set_bool "stop_before" (fun v -> np.stop_before <- v);
-    set_bool "lax_syntax" (fun v -> np.lax_syntax <- v);
     set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v);
     set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v);
-    current := np;
+    set_hd "background_color" (fun v -> np.background_color <- v);
+    set_hd "processing_color" (fun v -> np.processing_color <- v);
+    set_hd "processed_color" (fun v -> np.processed_color <- v);
+    current := np
 (*
     Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
 *)
-  with e ->
-    prerr_endline ("Could not load preferences ("^
-		   (Printexc.to_string e)^").")
-
-let split_string_format s =
-  try
-    let i = Util.string_index_from s 0 "%s" in
-    let pre = (String.sub s 0 i) in
-    let post = String.sub s (i+2) (String.length s - i - 2) in
-    pre,post
-  with Not_found -> s,""
 
 let configure ?(apply=(fun () -> ())) () =
+  let cmd_coqtop =
+    string
+      ~f:(fun s -> !current.cmd_coqtop <- if s = "AUTO" then None else Some s)
+      "       coqtop" (match !current.cmd_coqtop with |None -> "AUTO" | Some x -> x) in
   let cmd_coqc =
     string
       ~f:(fun s -> !current.cmd_coqc <- s)
@@ -332,7 +363,7 @@ let configure ?(apply=(fun () -> ())) () =
     let w = GMisc.font_selection () in
     w#set_preview_text
       "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z).";
-    box#pack w#coerce;
+    box#pack ~expand:true w#coerce;
     ignore (w#misc#connect#realize
 	      ~callback:(fun () -> w#set_font_name
 			   (Pango.Font.to_string !current.text_font)));
@@ -345,9 +376,67 @@ let configure ?(apply=(fun () -> ())) () =
 (*
 	 Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
 *)
-	 !change_font !current.text_font)
+	 !refresh_font_hook ())
       true
   in
+
+  let config_color =
+    let box = GPack.vbox () in
+    let table = GPack.table
+      ~row_spacings:5
+      ~col_spacings:5
+      ~border_width:2
+      ~packing:(box#pack ~expand:true) ()
+    in
+    let background_label = GMisc.label
+      ~text:"Background color"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:0) ()
+    in
+    let processed_label = GMisc.label
+      ~text:"Background color of processed text"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:1) ()
+    in
+    let processing_label = GMisc.label
+      ~text:"Background color of text being processed"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:2) ()
+    in
+    let () = background_label#set_xalign 0. in
+    let () = processed_label#set_xalign 0. in
+    let () = processing_label#set_xalign 0. in
+    let background_button = GButton.color_button
+      ~color:(Tags.color_of_string (!current.background_color))
+      ~packing:(table#attach ~left:1 ~top:0) ()
+    in
+    let processed_button = GButton.color_button
+      ~color:(Tags.get_processed_color ())
+      ~packing:(table#attach ~left:1 ~top:1) ()
+    in
+    let processing_button = GButton.color_button
+      ~color:(Tags.get_processing_color ())
+      ~packing:(table#attach ~left:1 ~top:2) ()
+    in
+    let reset_button = GButton.button
+      ~label:"Reset"
+      ~packing:box#pack ()
+    in
+    let reset_cb () =
+      background_button#set_color (Tags.color_of_string "cornsilk");
+      processing_button#set_color (Tags.color_of_string "light blue");
+      processed_button#set_color (Tags.color_of_string "light green");
+    in
+    let _ = reset_button#connect#clicked ~callback:reset_cb in
+    let label = "Color configuration" in
+    let callback () =
+      !current.background_color <- Tags.string_of_color background_button#color;
+      !current.processing_color <- Tags.string_of_color processing_button#color;
+      !current.processed_color <- Tags.string_of_color processed_button#color;
+      !refresh_background_color_hook ();
+      Tags.set_processing_color processing_button#color;
+      Tags.set_processed_color processed_button#color
+    in
+    custom ~label box callback true
+  in
+
 (*
   let show_toolbar =
     bool
@@ -376,7 +465,7 @@ let configure ?(apply=(fun () -> ())) () =
     bool
       ~f:(fun s ->
 	    !current.auto_complete <- s;
-	    !auto_complete s)
+	    !auto_complete_hook s)
       "Auto Complete" !current.auto_complete
   in
 
@@ -423,85 +512,85 @@ let configure ?(apply=(fun () -> ())) () =
       "Stop interpreting before the current point" !current.stop_before
   in
 
-  let lax_syntax =
-    bool
-      ~f:(fun s -> !current.lax_syntax <- s)
-      "Relax read-only constraint at end of command" !current.lax_syntax
-  in
-
   let vertical_tabs =
     bool
-      ~f:(fun s -> !current.vertical_tabs <- s)
+      ~f:(fun s -> !current.vertical_tabs <- s; !refresh_tabs_hook ())
       "Vertical tabs" !current.vertical_tabs
   in
 
   let opposite_tabs =
     bool
-      ~f:(fun s -> !current.opposite_tabs <- s)
+      ~f:(fun s -> !current.opposite_tabs <- s; !refresh_tabs_hook ())
       "Tabs on opposite side" !current.opposite_tabs
   in
 
   let encodings =
     combo
       "File charset encoding "
-      ~f:(fun s ->
-	    match s with
-	    | "UTF-8" ->
-		!current.encoding_use_utf8 <- true;
-		!current.encoding_use_locale <- false
-	    | "LOCALE" ->
-		!current.encoding_use_utf8 <- false;
-		!current.encoding_use_locale <- true
-	    | _ ->
-		!current.encoding_use_utf8 <- false;
-		!current.encoding_use_locale <- false;
-		!current.encoding_manual <- s;
-	 )
+      ~f:(fun s -> !current.encoding <- (inputenc_of_string s))
       ~new_allowed: true
-      ["UTF-8";"LOCALE";!current.encoding_manual]
-      (if !current.encoding_use_utf8 then "UTF-8"
-       else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual)
+      ("UTF-8"::"LOCALE":: match !current.encoding with
+	|Emanual s -> [s]
+	|_ -> []
+      )
+      (string_of_inputenc !current.encoding)
+  in
+  let read_project =
+    combo
+      "Project file options are"
+      ~f:(fun s -> !current.read_project <- project_behavior_of_string s)
+      ~editable:false
+      [string_of_project_behavior Subst_args;
+       string_of_project_behavior Append_args;
+       string_of_project_behavior Ignore_args]
+      (string_of_project_behavior !current.read_project)
+  in
+  let project_file_name =
+    string "Default name for project file"
+      ~f:(fun s -> !current.project_file_name <- s)
+      !current.project_file_name
   in
   let help_string =
     "restart to apply"
   in
+  let the_valid_mod = str_to_mod_list !current.modifiers_valid in
   let modifier_for_tactics =
     modifiers
-      ~allow:!current.modifiers_valid
-      ~f:(fun l -> !current.modifier_for_tactics <- l)
+      ~allow:the_valid_mod
+      ~f:(fun l -> !current.modifier_for_tactics <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for Tactics Menu"
-      !current.modifier_for_tactics
+      (str_to_mod_list !current.modifier_for_tactics)
   in
   let modifier_for_templates =
     modifiers
-      ~allow:!current.modifiers_valid
-      ~f:(fun l -> !current.modifier_for_templates <- l)
+      ~allow:the_valid_mod
+      ~f:(fun l -> !current.modifier_for_templates <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for Templates Menu"
-      !current.modifier_for_templates
+      (str_to_mod_list !current.modifier_for_templates)
   in
   let modifier_for_navigation =
     modifiers
-      ~allow:!current.modifiers_valid
-      ~f:(fun l -> !current.modifier_for_navigation <- l)
+      ~allow:the_valid_mod
+      ~f:(fun l -> !current.modifier_for_navigation <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for Navigation Menu"
-      !current.modifier_for_navigation
+      (str_to_mod_list !current.modifier_for_navigation)
   in
   let modifier_for_display =
     modifiers
-      ~allow:!current.modifiers_valid
-      ~f:(fun l -> !current.modifier_for_display <- l)
+      ~allow:the_valid_mod
+      ~f:(fun l -> !current.modifier_for_display <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for Display Menu"
-      !current.modifier_for_display
+      (str_to_mod_list !current.modifier_for_display)
   in
   let modifiers_valid =
     modifiers
-      ~f:(fun l -> !current.modifiers_valid <- l)
+      ~f:(fun l -> !current.modifiers_valid <- mod_list_to_str l)
       "Allowed modifiers"
-      !current.modifiers_valid
+      the_valid_mod
   in
   let cmd_editor =
     let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in
@@ -520,8 +609,7 @@ let configure ?(apply=(fun () -> ())) () =
       "netscape -remote \"openURL(%s)\"";
       "mozilla -remote \"openURL(%s)\"";
       "firefox -remote \"openURL(%s,new-windows)\" || firefox %s &";
-      "seamonkey -remote \"openURL(%s)\" || seamonkey %s &";
-      "open -a Safari %s &"
+      "seamonkey -remote \"openURL(%s)\" || seamonkey %s &"
     ] in
     combo
       ~help:"(%s for url)"
@@ -534,6 +622,8 @@ let configure ?(apply=(fun () -> ())) () =
   in
   let doc_url =
     let predefined = [
+      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";""]);
+      Coq_config.wwwrefman;
       use_default_doc_url
     ] in
     combo
@@ -545,11 +635,13 @@ let configure ?(apply=(fun () -> ())) () =
       !current.doc_url in
   let library_url =
     let predefined = [
+      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"stdlib";""]);
       Coq_config.wwwstdlib
     ] in
     combo
       "Library URL"
       ~f:(fun s -> !current.library_url <- s)
+      ~new_allowed: true
       (predefined@[if List.mem !current.library_url predefined then ""
                    else !current.library_url])
       !current.library_url
@@ -567,43 +659,46 @@ let configure ?(apply=(fun () -> ())) () =
     bool
       ~f:(fun s ->
 	    !current.contextual_menus_on_goal <- s;
-	    !contextual_menus_on_goal s)
+	    !contextual_menus_on_goal_hook s)
       "Contextual menus on goal" !current.contextual_menus_on_goal
   in
 
-  let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax;
+  let misc = [contextual_menus_on_goal;auto_complete;stop_before;
               vertical_tabs;opposite_tabs] in
 
 (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!!
    (shame on Benjamin) *)
   let cmds =
-    [Section("Fonts",
+    [Section("Fonts", Some `SELECT_FONT,
 	     [config_font]);
-     Section("Files",
+     Section("Colors", Some `SELECT_COLOR, [config_color]);
+     Section("Files", Some `DIRECTORY,
 	     [global_auto_revert;global_auto_revert_delay;
 	      auto_save; auto_save_delay; (* auto_save_name*)
 	      encodings;
 	     ]);
+     Section("Project", Some (`STOCK "gtk-page-setup"),
+	     [project_file_name;read_project;
+	     ]);
 (*
      Section("Appearance",
 	     config_appearance);
 *)
-     Section("Externals",
-	     [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;
-	      cmd_editor;
-	      cmd_browse;doc_url;library_url]);
-     Section("Tactics Wizard",
+     Section("Externals", None,
+	     [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
+	      cmd_print;cmd_editor;cmd_browse;doc_url;library_url]);
+     Section("Tactics Wizard", None,
 	     [automatic_tactics]);
-     Section("Shortcuts",
+     Section("Shortcuts", Some `PREFERENCES,
 	     [modifiers_valid; modifier_for_tactics;
 	      modifier_for_templates; modifier_for_display; modifier_for_navigation]);
-     Section("Misc",
+     Section("Misc", Some `ADD,
 	     misc)]
   in
 (*
   Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
 *)
-  let x = edit ~apply ~width:500 "Customizations" cmds in
+  let x = edit ~apply "Customizations" cmds in
 (*
   Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
 *)