coqide: corrections pour utf8 de coq. highlight synchrone=repare le bug autorepeat des paste. configuration des accel rateurs. les chaines peuvent contenir des points. Bug: les phrases ne peuvent pas contenir .\sep. Or c'est permis par les Notation.

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

4 files changed, 115 insertions, 0 deletions

diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml
index 73ee926e2c..62d3b9d5ab 100644
--- a/ide/utils/configwin.ml
+++ b/ide/utils/configwin.ml
@@ -37,6 +37,7 @@ let combo = Configwin_ihm.combo
 let custom = Configwin_ihm.custom
 let date = Configwin_ihm.date
 let hotkey = Configwin_ihm.hotkey
+let modifiers = Configwin_ihm.modifiers
 let html = Configwin_ihm.html
 
 let edit 
diff --git a/ide/utils/configwin.mli b/ide/utils/configwin.mli
index 1756554177..686b7c8ac0 100644
--- a/ide/utils/configwin.mli
+++ b/ide/utils/configwin.mli
@@ -211,6 +211,11 @@ val hotkey : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: ((Gdk.Tags.modifier list * int) -> unit) -> 
     string -> (Gdk.Tags.modifier list * int) -> parameter_kind
 
+val modifiers : ?editable: bool -> ?expand: bool -> ?help: string ->
+  ?allow:(Gdk.Tags.modifier list) ->
+  ?f: (Gdk.Tags.modifier list -> unit) -> 
+    string -> Gdk.Tags.modifier list -> parameter_kind
+
 
 (** [custom box f expand] creates a custom parameter, with
    the given [box], the [f] function is called when the user
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index f6c4e6daad..04d7c05ede 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -765,6 +765,58 @@ class hotkey_param_box param =
 	()
   end ;;
 
+class modifiers_param_box param =
+  let hbox = GPack.hbox () in
+  let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~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 _ = 
+    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 
+  in
+  let _ = we#set_text (KeyOption.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 (KeyOption.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
+    (** This method applies the new value of the parameter. *)
+    method apply =
+      let new_value = !value in
+      if new_value <> param.md_value then
+	let _ = param.md_f_apply new_value in
+	param.md_value <- new_value
+      else
+	()
+  end ;;
+
 (** This class is used to build a box for a date parameter.*)
 class date_param_box param =
   let v = ref param.date_value in
@@ -891,6 +943,10 @@ class configuration_box conf_struct (notebook : GPack.notebook) =
 		  let box = new hotkey_param_box p in
 		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 		  box
+	      |	Modifiers_param p ->
+		  let box = new modifiers_param_box p in
+		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+		  box
 	      |	Html_param p ->
 		  let box = new html_param_box p in
 		  let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
@@ -1093,6 +1149,10 @@ let box param_list buttons =
 	let box = new hotkey_param_box p in
 	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 	box
+    | Modifiers_param p ->
+	let box = new modifiers_param_box p in
+	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+	box
     | Html_param p ->
 	let box = new html_param_box p in
 	let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
@@ -1327,6 +1387,23 @@ let hotkey ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       hk_expand = expand ;
     } 
 
+let modifiers 
+  ?(editable=true) 
+  ?(expand=true) 
+  ?help 
+  ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5]) 
+  ?(f=(fun _ -> ())) label v =
+  Modifiers_param
+    {
+      md_label = label ;
+      md_help = help ;
+      md_value = v ;
+      md_editable = editable ;
+      md_f_apply = f ;
+      md_expand = expand ;
+      md_allow = allow ;
+    } 
+
 (** Create a custom param.*)
 let custom ?label box f expand =
   Custom_param
diff --git a/ide/utils/configwin_types.ml b/ide/utils/configwin_types.ml
index 4d8184ebd8..3e09de95f5 100644
--- a/ide/utils/configwin_types.ml
+++ b/ide/utils/configwin_types.ml
@@ -79,6 +79,26 @@ module KeyOption = struct
                      ) ^ s)
         in
         iter m ("-" ^ s)
+
+  let modifiers_to_string m =
+    let rec iter m s =
+      match m with
+          [] -> s
+        | c :: m ->
+            iter m ((
+                      match c with
+			  `CONTROL -> "<ctrl>"
+			| `SHIFT -> "<shft>"
+			| `LOCK -> "<lock>"
+			| `MOD1 -> "<alt>"
+			| `MOD2 -> "<mod2>"
+			| `MOD3 -> "<mod3>"
+			| `MOD4 -> "<mod4>"
+			| `MOD5 -> "<mod5>"
+			| _  -> raise Not_found
+                    ) ^ s)
+    in
+    iter m ""
 	  
   let value_to_key v =
     match v with
@@ -190,6 +210,17 @@ type hotkey_param = {
     hk_expand : bool ; (** expand or not *)
   } 
 
+type modifiers_param = {
+    md_label : string ; (** the label of the parameter *)
+    mutable md_value : Gdk.Tags.modifier list ; 
+             (** The value, as a list of modifiers and a key code *)
+    md_editable : bool ; (** indicates if the value can be changed *)
+    md_f_apply : Gdk.Tags.modifier list -> unit ;
+             (** the function to call to apply the new value of the paramter *)
+    md_help : string option ; (** optional help string *)
+    md_expand : bool ; (** expand or not *)
+    md_allow : Gdk.Tags.modifier list
+  } 
 
 (** This type represents the different kinds of parameters. *)
 type parameter_kind =
@@ -204,6 +235,7 @@ type parameter_kind =
   | Date_param of date_param
   | Font_param of font_param
   | Hotkey_param of hotkey_param
+  | Modifiers_param of modifiers_param
   | Html_param of string_param
 ;;