From 469cb750c6c1aa46f77b2a89a36f79f29aa97073 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 14 Dec 2015 13:33:47 +0100
Subject: Revert PMP's fix of #2498, which introduces an incompatibility with
 lablgtk 2.14. Debian ships with lablgtk 2.16 only since a few months, so we
 apply the fix to trunk instead.

This reverts commits:
490160d25d3caac1d2ea5beebbbebc959b1b3832.
ef8718a7fd3bcd960d954093d8c636525e6cc492.
6f9cc3aca5bb0e5684268a7283796a9272ed5f9d.
901a9b29adf507370732aeafbfea6718c1842f1b.
---
 ide/preferences.ml | 31 ++++---------------------------
 1 file changed, 4 insertions(+), 27 deletions(-)

(limited to 'ide')

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 90862d0647..01ce454834 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -711,61 +711,38 @@ let configure ?(apply=(fun () -> ())) () =
       ~f:(fun s -> current.project_file_name <- s)
       current.project_file_name
   in
-  let update_modifiers prefix mds =
-    let change ~path ~key ~modi ~changed =
-      if CString.is_sub prefix path 0 then
-        ignore (GtkData.AccelMap.change_entry ~key ~modi:mds ~replace:true path)
-    in
-    GtkData.AccelMap.foreach change
-  in
   let help_string =
     "restart to apply"
   in
   let the_valid_mod = str_to_mod_list current.modifiers_valid in
   let modifier_for_tactics =
-    let cb l =
-      current.modifier_for_tactics <- mod_list_to_str l;
-      update_modifiers "<Actions>/Tactics/" l
-    in
     modifiers
       ~allow:the_valid_mod
-      ~f:cb
+      ~f:(fun l -> current.modifier_for_tactics <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for Tactics Menu"
       (str_to_mod_list current.modifier_for_tactics)
   in
   let modifier_for_templates =
-    let cb l =
-      current.modifier_for_templates <- mod_list_to_str l;
-      update_modifiers "<Actions>/Templates/" l
-    in
     modifiers
       ~allow:the_valid_mod
-      ~f:cb
+      ~f:(fun l -> current.modifier_for_templates <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for Templates Menu"
       (str_to_mod_list current.modifier_for_templates)
   in
   let modifier_for_navigation =
-    let cb l =
-      current.modifier_for_navigation <- mod_list_to_str l;
-      update_modifiers "<Actions>/Navigation/" l
-    in
     modifiers
       ~allow:the_valid_mod
-      ~f:cb
+      ~f:(fun l -> current.modifier_for_navigation <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for Navigation Menu"
       (str_to_mod_list current.modifier_for_navigation)
   in
   let modifier_for_display =
-    let cb l =
-      current.modifier_for_display <- mod_list_to_str l;
-      update_modifiers "<Actions>/View/" l
-    in
     modifiers
       ~allow:the_valid_mod
-      ~f:cb
+      ~f:(fun l -> current.modifier_for_display <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for View Menu"
       (str_to_mod_list current.modifier_for_display)
-- 
cgit v1.2.3


From fa08993b9330623c8cb259ac8ebff93ecce9c2f6 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 14 Dec 2015 14:04:12 +0100
Subject: CoqIDE: add 'you need to restart CoqIDE after changing shortcuts'
 message

---
 ide/preferences.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 01ce454834..8988dbc60b 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -754,6 +754,13 @@ let configure ?(apply=(fun () -> ())) () =
       "Allowed modifiers"
       the_valid_mod
   in
+  let modifier_notice =
+    let b = GPack.hbox () in
+    let _lbl =
+      GMisc.label ~markup:"You need to <b>restart CoqIDE</b> after changing these settings"
+        ~packing:b#add () in
+    custom b (fun () -> ()) true
+  in
   let cmd_editor =
     let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in
     combo
@@ -855,7 +862,7 @@ let configure ?(apply=(fun () -> ())) () =
 	     [automatic_tactics]);
      Section("Shortcuts", Some `PREFERENCES,
 	     [modifiers_valid; modifier_for_tactics;
-	      modifier_for_templates; modifier_for_display; modifier_for_navigation]);
+	      modifier_for_templates; modifier_for_display; modifier_for_navigation; modifier_notice]);
      Section("Misc", Some `ADD,
 	     misc)]
   in
-- 
cgit v1.2.3


From 2ab8455cffef4097a441eb6befaa29f6f3076824 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Jul 2015 21:25:15 +0200
Subject: Fixing little bug of coq_makefile with unterminated comment.

Force failing when reaching end of file with unterminated comment when
parsing Make (project) file.
---
 ide/project_file.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'ide')

diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index f7279f9cfe..152f76cc0e 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -28,6 +28,7 @@ let rec parse_string = parser
 and parse_string2 = parser
   | [< ''"' >] -> ""
   | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
+  | [< >] -> raise Parsing_error
 and parse_skip_comment = parser
   | [< ''\n'; s >] -> s
   | [< 'c; s >] -> parse_skip_comment s
-- 
cgit v1.2.3