From 3fa1bf32ec323ce03a7fa818a8daccb78b862ca6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 25 Jan 2015 17:38:52 +0100
Subject: Fixing bug #3947.

---
 ide/wg_Find.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index b6f63a3ba1..b6b1ea6bcb 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -8,6 +8,8 @@
 
 type mode = [ `FIND | `REPLACE ]
 
+let b2c = Ideutils.byte_offset_to_char_offset
+
 class finder name (view : GText.view) =
   
   let widget = Wg_Detachable.detachable
@@ -85,8 +87,8 @@ class finder name (view : GText.view) =
       try
         let i = Str.search_backward regexp text (String.length text - 1) in
         let j = Str.match_end () in
-        Some(view#buffer#start_iter#forward_chars i,
-             view#buffer#start_iter#forward_chars j)
+        Some(view#buffer#start_iter#forward_chars (b2c text i),
+             view#buffer#start_iter#forward_chars (b2c text j))
       with Not_found -> None
     
     method private forward_search starti =
@@ -95,7 +97,7 @@ class finder name (view : GText.view) =
       try
         let i = Str.search_forward regexp text 0 in
         let j = Str.match_end () in
-        Some(starti#forward_chars i, starti#forward_chars j)
+        Some(starti#forward_chars (b2c text i), starti#forward_chars (b2c text j))
       with Not_found -> None
 
     method replace_all () =
-- 
cgit v1.2.3


From 3d6b9a7ab992559493b89e174549734dff401703 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 25 Jan 2015 17:49:35 +0100
Subject: Made replacing of text in CoqIDE atomic w.r.t. the undo/redo.

---
 ide/wg_Find.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index b6b1ea6bcb..a0949ca0c8 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -63,8 +63,10 @@ class finder name (view : GText.view) =
     method replace () =
       if self#may_replace () then
         let txt = self#get_selected_word () in
+        let () = view#buffer#begin_user_action () in
         let _ = view#buffer#delete_selection () in
         let _ = view#buffer#insert_interactive (self#replacement txt) in
+        let () = view#buffer#end_user_action () in
         self#find_forward ()
       else self#find_forward ()
 
@@ -117,7 +119,9 @@ class finder name (view : GText.view) =
           let () = view#buffer#delete_mark (`MARK stop_mark) in
           replace_at next
       in
-      replace_at view#buffer#start_iter
+      let () = view#buffer#begin_user_action () in
+      let () = replace_at view#buffer#start_iter in
+      view#buffer#end_user_action ()
 
     method private set_not_found () =
       find_entry#misc#modify_base [`NORMAL, `NAME "#F7E6E6"];
-- 
cgit v1.2.3