Merge branch 'v8.5'

3 files changed, 12 insertions, 7 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index ac38f1ea5a..f4b81a241b 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -123,7 +123,7 @@ let annotate phrase =
     let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
     Vernac.parse_sentence (pa,None)
   in
-  let (_, _, xml) =
+  let (_, xml) =
     Richprinter.richpp_vernac ast
   in
   xml
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index d2305b58c1..a869442696 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -175,10 +175,7 @@ let select_file_for_save ~title ?filename () =
   file_chooser#add_select_button_stock `SAVE `SAVE ;
   file_chooser#add_filter (filter_coq_files ());
   file_chooser#add_filter (filter_all_files ());
-  (* this line will be used when a lablgtk >= 2.10.0 is the default
-     on most distributions:
-     file_chooser#set_do_overwrite_confirmation true;
-  *)
+  file_chooser#set_do_overwrite_confirmation true;
   file_chooser#set_default_response `SAVE;
   let dir,filename = match filename with
     |None -> !last_dir, ""
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 1f3990708a..5d21efd956 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -186,11 +186,19 @@ object(self)
 
   method undo () =
     Minilib.log "UNDO";
-    self#with_lock_undo self#perform_undo ();
+    self#with_lock_undo begin fun () ->
+      buffer#begin_user_action ();
+      self#perform_undo ();
+      buffer#end_user_action ()
+    end ()
 
   method redo () =
     Minilib.log "REDO";
-    self#with_lock_undo self#perform_redo ();
+    self#with_lock_undo begin fun () ->
+      buffer#begin_user_action ();
+      self#perform_redo ();
+      buffer#end_user_action ()
+    end ()
 
   method process_begin_user_action () =
     (* Push a new level of event on history stack *)