diff options
| author |  Lionel Rieg <lionel.rieg@ensiie.fr> | 2016-06-02 15:24:35 +0200 |
|---|---|---|
| committer |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-06-02 15:44:40 +0200 |
| commit | 9bbad8a588a98fc4836809f73db0caf7efa9e346 (patch) | |
| tree | 2dba51affb211a45e8096538d5705b854c5a70e3 | |
| parent | 4c66c7f9c370d2088dfa064e77f45b869c672e98 (diff) | |
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.
| -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 |