diff options
| author | Pierre-Marie Pédrot | 2021-04-19 19:06:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-04-19 19:06:18 +0200 |
| commit | d89f5c935af6e6055691b9980c7dfdfa481b6c4f (patch) | |
| tree | ad9da0bb302c58b5f015ef104447579ac8fb711f /ide/coqide/configwin_ihm.ml | |
| parent | b53642ec813178fedd3e646832e7c033b8163f52 (diff) | |
| parent | 32cc7cb03f879d089e226958ab8e89cbcde79d10 (diff) | |
Merge PR #14060: Coqide: on MacOS X, allow the command (⌘) key to be set/unset as a modifier
Reviewed-by: ppedrot
Diffstat (limited to 'ide/coqide/configwin_ihm.ml')
| -rw-r--r-- | ide/coqide/configwin_ihm.ml | 7 |
1 files changed, 6 insertions, 1 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 { |