From 0400385142aaac484e0b2917c9bb41181c087d07 Mon Sep 17 00:00:00 2001 From: Tony Garnock-Jones Date: Mon, 26 Sep 2016 16:02:46 -0400 Subject: [PATCH] Window list widgetry --- gui.rkt | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/gui.rkt b/gui.rkt index 9ba7659..20de493 100644 --- a/gui.rkt +++ b/gui.rkt @@ -500,6 +500,22 @@ (on (message (button-click 'start-button (mouse-state $mx $my _ _ _))) (send! (pop-up-menu-trigger 'system-menu mx my 0 1 'left-up))))) +(actor #:name 'window-list-monitor + (during/actor (window-state $id $title _) + (field [x 0] [y 0]) + (define reqsize + (parameterize ((theme-button-y-padding 8) + (theme-button-min-height 0) + (theme-button-background-color (hsv->color 240 1 0.6))) + (pushbutton title x y #:id (list 'window-list id) #:parent 'toolbar + #:trigger-event 'left-down))) + (during (layout-solution 'toolbar (horizontal-layout `(-5.0 ,id)) reqsize + (rectangle $l $t $w $h)) + (x l) + (y t) + (on (message (button-click (list 'window-list id) _)) + (send! (raise-widget id)))))) + (actor #:name 'clock (field [now (current-seconds)]) (on (message (inbound (frame-event _ $timestamp _ _)))