From 73942fcfa801d940f4786f1cd834e321ac725be9 Mon Sep 17 00:00:00 2001 From: Vincent St-Amour Date: Mon, 23 Jul 2012 17:17:49 -0400 Subject: [PATCH] Wrap highlighting in an edit sequence. Speeds up display. --- collects/typed-racket/optimizer/tool/tool.rkt | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/collects/typed-racket/optimizer/tool/tool.rkt b/collects/typed-racket/optimizer/tool/tool.rkt index 29ab44788c..41e43aa0e4 100644 --- a/collects/typed-racket/optimizer/tool/tool.rkt +++ b/collects/typed-racket/optimizer/tool/tool.rkt @@ -63,7 +63,8 @@ (mixin (text:basic<%> drracket:unit:definitions-text<%>) () (inherit highlight-range unhighlight-range get-tab get-canvas get-pos/text - position-line line-end-position) + position-line line-end-position + begin-edit-sequence end-edit-sequence) (define highlights '()) ; (listof `(,start ,end ,popup-fun)) (define clear-thunks '()) ; list of thunks that clear highlights @@ -124,9 +125,11 @@ (apply max (cons 0 (map report-entry-badness report)))) (unless (= max-badness 0) ; no missed opts, color table code would error (set! color-table (make-color-table max-badness))) + (begin-edit-sequence) (set! clear-thunks (for/fold ([res '()]) ([r (in-list report)]) (append (highlight-entry r) res))) + (end-edit-sequence) (set! on? #t)) (define/public (clear-highlights)