suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Refactoring.

Browse Source
This commit is contained in:
Vincent St-Amour 2012-07-25 11:41:12 -04:00
parent 7b72ddb7bf
commit d9f97d079f
1 changed files with 11 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
collects/typed-racket/optimizer/tool/tool.rkt
View File

@ -216,9 +216,10 @@
(inherit set-show-menu-sort-key get-current-tab (inherit set-show-menu-sort-key get-current-tab
get-definitions-text get-interactions-text) get-definitions-text get-interactions-text)
;; view menu
(define/public (get-optimization-coach-menu-item) (define/public (get-optimization-coach-menu-item)
optimization-coach-menu-item) optimization-coach-menu-item)
(define/override (add-show-menu-items show-menu) (define/override (add-show-menu-items show-menu)
(super add-show-menu-items show-menu) (super add-show-menu-items show-menu)
(set! optimization-coach-menu-item (set! optimization-coach-menu-item
@ -239,13 +240,6 @@
(send (send tab get-defs) clear-highlights) (send (send tab get-defs) clear-highlights)
(optimization-coach-callback this)))])) (optimization-coach-callback this)))]))
(set-show-menu-sort-key optimization-coach-menu-item 403)) (set-show-menu-sort-key optimization-coach-menu-item 403))
(define/augment (on-tab-change old-tab new-tab)
(send old-tab hide-optimization-coach-panel #f) ; don't close it
(when (send new-tab optimization-coach-visible?)
;; if it was open before
(send new-tab show-optimization-coach-panel)))
(define optimization-coach-menu-item #f) (define optimization-coach-menu-item #f)
@ -259,6 +253,15 @@
menu pos text)) menu pos text))
(old menu editor event)))) (old menu editor event))))
;; tab switching
(define/augment (on-tab-change old-tab new-tab)
(send old-tab hide-optimization-coach-panel #f) ; don't close it
(when (send new-tab optimization-coach-visible?)
;; if it was open before
(send new-tab show-optimization-coach-panel)))
;; entry point ;; entry point
(define/public (optimization-coach-callback) (define/public (optimization-coach-callback)
(define definitions (get-definitions-text)) (define definitions (get-definitions-text))