Coqide: on MacOS X, allow the command key to be set/unset as a modifier.

This is done by:
- allowing the <Meta> gtk modifier (gtk internal name for Command) to
  be used as a modifier by default on MacOS X
- printing it <cmd> in the preference window when on MacOS X

2 files changed, 16 insertions, 6 deletions

diff --git a/ide/coqide/configwin_ihm.ml b/ide/coqide/configwin_ihm.ml
index e768131dcf..da1553d751 100644
--- a/ide/coqide/configwin_ihm.ml
+++ b/ide/coqide/configwin_ihm.ml
@@ -31,6 +31,10 @@ let set_help_tip wev = function
   | None -> ()
   | Some help -> GtkBase.Widget.Tooltip.set_text wev#as_widget help
 
+let select_arch m m_osx =
+  if Coq_config.arch = "Darwin" then m_osx else m
+
+(* How the modifiers are named in the preference box *)
 let modifiers_to_string m =
   let rec iter m s =
     match m with
@@ -41,6 +45,7 @@ let modifiers_to_string m =
                         `CONTROL -> "<ctrl>"
                       | `SHIFT -> "<shft>"
                       | `LOCK -> "<lock>"
+                      | `META -> select_arch "<meta>" "<cmd>"
                       | `MOD1 -> "<alt>"
                       | `MOD2 -> "<mod2>"
                       | `MOD3 -> "<mod3>"
@@ -773,7 +778,7 @@ let modifiers
   ?(editable=true)
   ?(expand=true)
   ?help
-  ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5])
+  ?(allow=[`CONTROL;`SHIFT;`LOCK;`META;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5])
   ?(f=(fun _ -> ())) label v =
   Modifiers_param
     {
diff --git a/ide/coqide/preferences.ml b/ide/coqide/preferences.ml
index 5a77f4ebcf..486a279de0 100644
--- a/ide/coqide/preferences.ml
+++ b/ide/coqide/preferences.ml
@@ -321,18 +321,21 @@ let attach_modifiers (pref : string preference) prefix =
   in
   pref#connect#changed ~callback:cb
 
-let select_arch m m_osx =
-  if Coq_config.arch = "Darwin" then m_osx else m
-
 let modifier_for_navigation =
   new preference ~name:["modifier_for_navigation"]
-    ~init:(select_arch "<Control>" "<Control><Primary>") ~repr:Repr.(string)
+    (* Note: on Darwin, this will give "<Control><Meta>", i.e. Ctrl and Command; on other
+    architectures, "<Primary>" binds to "<Control>" so it will give "<Control>" alone *)
+    ~init:"<Control><Primary>" ~repr:Repr.(string)
 
 let modifier_for_templates =
   new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string)
 
+let select_arch m m_osx =
+  if Coq_config.arch = "Darwin" then m_osx else m
+
 let modifier_for_display =
   new preference ~name:["modifier_for_display"]
+   (* Note: <Primary> (i.e. <Meta>, i.e. "Command") on Darwin, i.e. MacOS X, but <Alt> elsewhere *)
     ~init:(select_arch "<Alt><Shift>" "<Primary><Shift>")~repr:Repr.(string)
 
 let modifier_for_queries =
@@ -348,7 +351,9 @@ let attach_modifiers_callback () =
   ()
 
 let modifiers_valid =
-  new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string)
+  new preference ~name:["modifiers_valid"]
+   (* Note: <Primary> is providing <Meta> (i.e. "Command") for Darwin, i.e. MacOS X *)
+    ~init:"<Alt><Control><Shift><Primary>" ~repr:Repr.(string)
 
 let browser_cmd_fmt =
  try