diff options
| author | Hugo Herbelin | 2019-04-27 12:18:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-04-30 12:50:47 +0200 |
| commit | dda4e65e530bd0e4a3ada165fdc752e1a217da8b (patch) | |
| tree | 1fdf5842a31aa24050be4f8d6cfa5a58918a7796 /ide | |
| parent | 714d745858b031e58c5d089799d017eb092543c0 (diff) | |
CoqIDE: Adding MacOS X support for Meta-based nano-PG keys.
In practice, most of Alt modified keys are used on MacOS X keyboards
for special characters and many Command modified keys are used for
MacOS standard actions.
So, we propose to use Ctrl-Command- as a prefix for the Meta-based
nano-PG shortcuts. E.g. Ctrl-Command-e would go the end of the
sentence.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/nanoPG.ml | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 89bf07ce23..0cb39c8d75 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -65,7 +65,13 @@ type 'c entry = { } let mC = [`CONTROL] -let mM = [`MOD1] +let mM = + if Coq_config.arch = "Darwin" then + (* We add both MOD2 and META because both are + returned when pressing Command on MacOS X *) + [`CONTROL;`MOD2;`META] + else + [`MOD1] let mod_of t x = let y = GdkEvent.Key.state t in @@ -73,9 +79,13 @@ let mod_of t x = List.for_all (fun m -> List.mem m x) y let pr_keymod l = - if l = mC then "Ctrl-" - else if l = mM then "Meta-" - else "" + if l = mC then + "Ctrl-" + else + if l = mM then + if Coq_config.arch = "Darwin" then "Ctrl-Cmd-" else "Meta-" + else + "" let mkE ?(mods=mC) key keyname doc ?(alias=[]) contents = List.map (fun (mods, key, keyname) -> { mods; key; keyname; doc; contents }) |