diff options
| author | Hugo Herbelin | 2021-04-02 19:19:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2021-04-18 19:18:45 +0200 |
| commit | 32cc7cb03f879d089e226958ab8e89cbcde79d10 (patch) | |
| tree | 26d82a9ee92b968e0491ea6366681017b2bf7e57 /ide/coqide/configwin_ihm.ml | |
| parent | 3167c19fbca224c4d88665ef47dedbd483671f84 (diff) | |
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
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 { |