aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-04 21:39:18 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-04 21:39:18 +0000
commitf0b936e7cb90000f5db6272b926cb13dc1a5c055 (patch)
tree63a5fefc70912f436c08b75f2e5813e62f407a93 /ide
parent0187193260a57e6bac8fcde8eb0e66ccf3f37b9b (diff)
Fix coqide compilation with lablgtk 2.16
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15772 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-rw-r--r--ide/preferences.ml4
-rw-r--r--ide/utils/okey.ml10
2 files changed, 13 insertions, 1 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 0866563f7..9e226708f 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -41,6 +41,10 @@ let mod_to_str (m:Gdk.Tags.modifier) =
| `MOD5 -> "<Mod5>"
| `CONTROL -> "<Control>"
| `SHIFT -> "<Shift>"
+ | `HYPER -> "<Hyper>"
+ | `META -> "<Meta>"
+ | `RELEASE -> ""
+ | `SUPER -> "<Super>"
| `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> ""
let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l
diff --git a/ide/utils/okey.ml b/ide/utils/okey.ml
index 6b174ecbe..580f1fbcb 100644
--- a/ide/utils/okey.ml
+++ b/ide/utils/okey.ml
@@ -47,6 +47,10 @@ let int_of_modifier = function
| `BUTTON3 -> 1024
| `BUTTON4 -> 2048
| `BUTTON5 -> 4096
+ | `HYPER -> 1 lsl 22
+ | `META -> 1 lsl 20
+ | `RELEASE -> 1 lsl 30
+ | `SUPER -> 1 lsl 21
let print_modifier l =
List.iter
@@ -65,7 +69,11 @@ let print_modifier l =
| `BUTTON2 -> "B2"
| `BUTTON3 -> "B3"
| `BUTTON4 -> "B4"
- | `BUTTON5 -> "B5")
+ | `BUTTON5 -> "B5"
+ | `HYPER -> "HYPER"
+ | `META -> "META"
+ | `RELEASE -> ""
+ | `SUPER -> "SUPER")
m)^" ")
)
l;