From d039e69266b5f0ccdac05ac7358008f46798efcb Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 7 Dec 2012 15:19:08 +0000
Subject: 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
---
 ide/coqide.ml | 20 ++++++--------------
 1 file 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)
               )
     );
-- 
cgit v1.2.3