diff --git a/collects/typed-racket/optimizer/tool/tool.rkt b/collects/typed-racket/optimizer/tool/tool.rkt index 653199a9c3..2b50aa6aaa 100644 --- a/collects/typed-racket/optimizer/tool/tool.rkt +++ b/collects/typed-racket/optimizer/tool/tool.rkt @@ -145,10 +145,13 @@ (set! highlights '()) (set! on? #f)) + (define (clear-and-close) + (when on? + (send+ this (get-tab) (get-frame) (close-optimization-coach)))) (define/augment (on-insert start len) - (clear-highlights)) + (clear-and-close)) (define/augment (on-delete start len) - (clear-highlights)) + (clear-and-close)) (define/public (build-optimization-coach-popup-menu menu pos text) (and pos