From dda4e65e530bd0e4a3ada165fdc752e1a217da8b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 27 Apr 2019 12:18:17 +0200
Subject: 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.
---
 ide/nanoPG.ml | 18 ++++++++++++++----
 1 file 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 })
-- 
cgit v1.2.3