Coqide: better removal of the error red tag

 Instead of trying to limit the retag to the visible zone
 (which may be wrong if the user has scrolled), we remove
 the red error tag from the whole buffer (this isn't costly).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16038 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 14 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 3001917bc4..be918833f8 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -903,24 +903,16 @@ object(self)
               )
     );
     ignore (input_buffer#connect#begin_user_action
-	      ~callback:(fun () ->
-		           let here = input_buffer#get_iter_at_mark `INSERT in
-			   input_buffer#move_mark (`NAME "prev_insert") here
-	      )
+              ~callback:(fun () ->
+                let where = self#get_insert in
+                input_buffer#move_mark (`NAME "prev_insert") ~where;
+                let start = self#get_start_of_input in
+                let stop = input_buffer#end_iter in
+                input_buffer#remove_tag Tags.Script.error ~start ~stop)
     );
     ignore (input_buffer#connect#end_user_action
               ~callback:(fun () ->
                 last_modification_time <- Unix.time ();
-                let r = input_view#visible_rect in
-                let stop =
-                  input_view#get_iter_at_location
-                    ~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r)
-                    ~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r)
-                in
-                input_buffer#remove_tag
-                  Tags.Script.error
-                  ~start:self#get_start_of_input
-                  ~stop;
                 tag_on_insert (input_buffer :> GText.buffer)
               )
     );