aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/ide_slave.ml2
-rw-r--r--ide/ideutils.ml5
-rw-r--r--ide/wg_ScriptView.ml12
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 *)