Change the customization of modifiers (bug #2210)

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

3 files changed, 17 insertions, 44 deletions

diff --git a/ide/preferences.ml b/ide/preferences.ml
index bb35ed246c..4e87d1df44 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -90,7 +90,6 @@ type pref =
       mutable window_height :int;
       mutable query_window_width : int;
       mutable query_window_height : int;
-      mutable fold_delay_ms : int;
 (*
       mutable use_utf8_notation : bool;
 *)
@@ -147,7 +146,6 @@ let (current:pref ref) =
     window_height = 600;
     query_window_width = 600;
     query_window_height = 400;
-    fold_delay_ms = 400;
 (*
     use_utf8_notation = false;
 *)
@@ -218,7 +216,6 @@ let save_pref () =
     add "window_width" [string_of_int p.window_width] ++
     add "query_window_height" [string_of_int p.query_window_height] ++
     add "query_window_width" [string_of_int p.query_window_width] ++
-    add "fold_delay_ms" [string_of_int p.fold_delay_ms] ++
     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] ++
@@ -282,7 +279,6 @@ let load_pref () =
     set_int "window_height" (fun v -> np.window_height <- v);
     set_int "query_window_width" (fun v -> np.query_window_width <- v);
     set_int "query_window_height" (fun v -> np.query_window_height <- v);
-    set_int "fold_delay_ms" (fun v -> np.fold_delay_ms <- 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);
@@ -416,14 +412,6 @@ let configure ?(apply=(fun () -> ())) () =
       (string_of_int !current.auto_save_delay)
   in
 
-  let fold_delay_ms =
-    string
-      ~f:(fun s -> !current.fold_delay_ms <-
-                   (try int_of_string s with _ -> 300))
-      "double click delay to trigger folding (ms)"
-      (string_of_int !current.fold_delay_ms)
-  in
-
   let stop_before =
     bool
       ~f:(fun s -> !current.stop_before <- s)
@@ -470,7 +458,7 @@ let configure ?(apply=(fun () -> ())) () =
        else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual)
   in
   let help_string =
-    "Press a set of modifiers and an extra key together (needs then a restart to apply!)"
+    "restart to apply"
   in
   let modifier_for_tactics =
     modifiers
@@ -603,7 +591,7 @@ let configure ?(apply=(fun () -> ())) () =
 	     [automatic_tactics]);
      Section("Shortcuts",
 	     [modifiers_valid; modifier_for_tactics;
-	      modifier_for_templates; modifier_for_display; modifier_for_navigation; fold_delay_ms]);
+	      modifier_for_templates; modifier_for_display; modifier_for_navigation]);
      Section("Misc",
 	     misc)]
   in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 2094443b40..6ee7918fed 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -49,7 +49,6 @@ type pref =
       mutable window_height : int;
       mutable query_window_width : int;
       mutable query_window_height : int;
-      mutable fold_delay_ms : int;
 (*
       mutable use_utf8_notation : bool;
 *)
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index eed23aaca9..3833acfada 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -802,41 +802,27 @@ class hotkey_param_box param (tt:GData.tooltips) =
 
 class modifiers_param_box param =
   let hbox = GPack.hbox () in
-  let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
+  let wev = GBin.event_box ~packing: (hbox#pack ~expand:true ~fill:true ~padding: 2) () in
   let _wl = GMisc.label ~text: param.md_label ~packing: wev#add () in
-  let we = GEdit.entry
-      ~editable: false
-      ~packing: (hbox#pack ~expand: param.md_expand ~padding: 2)
-      ()
-  in
   let value = ref param.md_value in
+  let _ = List.map (fun modifier ->
+                      let but = GButton.toggle_button
+                                  ~label:(Configwin_types.modifiers_to_string [modifier])
+                                  ~active:(List.mem modifier param.md_value)
+                                  ~packing:(hbox#pack ~expand:false) () in
+                      ignore (but#connect#toggled
+                                (fun _ -> if but#active then value := modifier::!value
+                                 else value := List.filter ((<>) modifier) !value)))
+            param.md_allow
+  in
   let _ =
     match param.md_help with
       None -> ()
     | Some help ->
-	let tooltips = GData.tooltips () in
-	ignore (hbox#connect#destroy ~callback: tooltips#destroy);
-	tooltips#set_tip wev#coerce ~text: help ~privat: help
+       let tooltips = GData.tooltips () in
+       ignore (hbox#connect#destroy ~callback: tooltips#destroy);
+       tooltips#set_tip wev#coerce ~text: help ~privat: help
   in
-  let _ = we#set_text (Configwin_types.modifiers_to_string param.md_value) in
-  let mods_we_care = param.md_allow in
-  let capture ev =
-    let modifiers = GdkEvent.Key.state ev in
-    let mods = List.filter
-	(fun m -> (List.mem m mods_we_care))
-	modifiers
-    in
-    value := mods;
-    we#set_text (Configwin_types.modifiers_to_string !value);
-    false
-  in
-  let _ =
-    if param.md_editable then
-      ignore (we#event#connect#key_press capture)
-    else
-      ()
-  in
-
   object (self)
     (** This method returns the main box ready to be packed. *)
     method box = hbox#coerce
@@ -1411,7 +1397,7 @@ let modifiers
   ?(editable=true)
   ?(expand=true)
   ?help
-  ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5])
+  ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5])
   ?(f=(fun _ -> ())) label v =
   Modifiers_param
     {