Avoid refreshing the segment widget each time a sentence is added.

This brings a 10x speedup for going at the end of large .v files.

1 files changed, 7 insertions, 2 deletions

diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 47fdeb127..0d047b54e 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -59,6 +59,8 @@ object (self)
   val mutable default : color = `WHITE
   val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
   val clicked = new GUtil.signal ()
+  val mutable need_refresh = false
+  val refresh_timer = Ideutils.mktimer ()
 
   initializer
     box#misc#set_size_request ~height ();
@@ -85,13 +87,15 @@ object (self)
     in
     let _ = eventbox#event#connect#button_press clicked_cb in
     (** Initial pixmap *)
-    draw#set_pixmap pixmap
+    draw#set_pixmap pixmap;
+    refresh_timer.Ideutils.run ~ms:300
+      ~callback:(fun () -> if need_refresh then self#refresh (); true)
 
   method set_model md =
     model <- Some md;
     let changed_cb = function
     | `INSERT | `REMOVE ->
-      if self#misc#visible then self#refresh ()
+      if self#misc#visible then need_refresh <- true
     | `SET (i, color) ->
       if self#misc#visible then self#fill_range color i (i + 1)
     in
@@ -122,6 +126,7 @@ object (self)
   method private refresh () = match model with
   | None -> ()
   | Some md ->
+    need_refresh <- false;
     pixmap#set_foreground default;
     pixmap#rectangle ~x:0 ~y:0 ~width ~height ~filled:true ();
     let make (k, cur, accu) v = match cur with