From 72c1fefcfb3f0dff02005034685f6b58ff84b3cc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 27 Sep 2016 18:28:48 +0200
Subject: Fix bug #4553: CoqIDE gives warnings about deprecated GTK features.

---
 ide/coqide.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'ide')

diff --git a/ide/coqide.ml b/ide/coqide.ml
index d1a799a773..450bfcdfb1 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -937,7 +937,6 @@ let emit_to_focus window sgn =
 let build_ui () =
   let w = GWindow.window
     ~wm_class:"CoqIde" ~wm_name:"CoqIde"
-    ~allow_grow:true ~allow_shrink:true
     ~width:window_width#get ~height:window_height#get
     ~title:"CoqIde" ()
   in
-- 
cgit v1.2.3


From 9b1c4576d89014d686bc10f13455a52de8d793bf Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 28 Sep 2016 16:46:32 +0200
Subject: Make error message more helpful.

CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options.---
 ide/ide_slave.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 1f933fb8a5..239fc587ce 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -98,7 +98,7 @@ let coqide_cmd_checks (loc,ast) =
   if is_debug ast then
     user_error "Debug mode not available within CoqIDE";
   if is_known_option ast then
-    msg_warning (strbrk"This will not work. Use CoqIDE display menu instead");
+    msg_warning (strbrk"This will not work. Use CoqIDE view menu instead");
   if Vernac.is_navigation_vernac ast || is_undo ast then
     msg_warning (strbrk "Rather use CoqIDE navigation instead");
   if is_query ast then
-- 
cgit v1.2.3


From d907342e31930eb2b8af7c9cc12bd0ddc7c00709 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 28 Sep 2016 17:00:09 +0200
Subject: Do not stop propagation of signals when Coq is busy (bug #3941).

When inserting a character in an already processed buffer, a message is
sent to Coq so that the proof is backtracked and the character is
inserted. If a second character is inserted while Coq is still busy with
the first message, the action is canceled, but the signal is no longer
dropped so that the second character is properly inserted.
---
 ide/session.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/session.ml b/ide/session.ml
index e998337604..fc6340d283 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -108,10 +108,10 @@ let set_buffer_handlers
     let id = ref 0 in
     fun () -> incr id; !id in
   let running_action = ref None in
-  let cancel_signal reason =
+  let cancel_signal ?(stop_emit=true) reason =
     Minilib.log ("user_action cancelled: "^reason);
     action_was_cancelled := true;
-    GtkSignal.stop_emit () in
+    if stop_emit then GtkSignal.stop_emit () in
   let del_mark () =
     try buffer#delete_mark (`NAME "target")
     with GText.No_such_mark _ -> () in
@@ -124,7 +124,7 @@ let set_buffer_handlers
       fun () -> (* If Coq is busy due to the current action, we don't cancel *)
         match !running_action with
         | Some aid when aid = action -> ()
-        | _ -> cancel_signal "Coq busy" in
+        | _ -> cancel_signal ~stop_emit:false "Coq busy" in
     Coq.try_grab coqtop action fallback in
   let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in
   let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in
-- 
cgit v1.2.3


From edb55a94fc5c0473e57f5a61c0c723194c2ff414 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 27 Sep 2016 17:15:10 +0200
Subject: Fix bug #4798: compat notations should not modify the parser.

This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
---
 ide/texmacspp.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 53a29008ad..9de1df9f1e 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -189,7 +189,8 @@ match sm with
       end
   | SetEntryType (s, _) -> ["entrytype", s]
   | SetOnlyPrinting -> ["onlyprinting", ""]
-  | SetOnlyParsing v -> ["compat", Flags.pr_version v]
+  | SetOnlyParsing -> ["onlyparsing", ""]
+  | SetCompatVersion v -> ["compat", Flags.pr_version v]
   | SetFormat (system, (loc, s)) ->
       let start, stop = unlock loc in
       ["format-"^system, s; "begin", start; "end", stop]
-- 
cgit v1.2.3