From 205bfad25b144f7a6a4e869d8253ec8471d52108 Mon Sep 17 00:00:00 2001 From: Lionel Rieg Date: Thu, 2 Jun 2016 15:24:35 +0200 Subject: 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. --- ide/wg_Segment.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'ide/wg_Segment.ml') diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index c2799e40b..dbc1740ef 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -60,6 +60,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 (); @@ -88,13 +90,15 @@ object (self) let cb show = if show then self#misc#show () else self#misc#hide () in stick show_progress_bar self cb; (** 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 @@ -125,6 +129,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 -- cgit v1.2.3