diff options
Diffstat (limited to 'ide/wg_Segment.ml')
-rw-r--r-- | ide/wg_Segment.ml | 9 |
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 |