Common margins for all panes

(Is this the right place to put it?)
2015-07-19 22:29:47 +02:00 · 2015-07-19 22:29:47 +02:00 · 265a855217
parent 8c0fbca360
commit 265a855217
1 changed files with 3 additions and 0 deletions
--- a/basis/ui/tools/common/common.factor
+++ b/basis/ui/tools/common/common.factor
@ -38,3 +38,6 @@ SLOT: scroller

 : com-scroll-down ( tool -- )
    scroller>> scroll-down-line ;
+
+: margins ( child -- border ) 
+    { 9 9 } <filled-border> ;