ui.tools.listener: change to just reset line-height so it can be recomputed lazily when needed.
parent
6de6cb687f
commit
021e595c58
|
@ -11,7 +11,7 @@ threads tools.errors.model ui ui.commands ui.gadgets
|
||||||
ui.gadgets.editors ui.gadgets.glass ui.gadgets.labeled
|
ui.gadgets.editors ui.gadgets.glass ui.gadgets.labeled
|
||||||
ui.gadgets.panes ui.gadgets.scrollers ui.gadgets.status-bar
|
ui.gadgets.panes ui.gadgets.scrollers ui.gadgets.status-bar
|
||||||
ui.gadgets.toolbar ui.gadgets.tracks ui.gestures ui.operations
|
ui.gadgets.toolbar ui.gadgets.tracks ui.gestures ui.operations
|
||||||
ui.pens.solid ui.text ui.theme ui.tools.browser ui.tools.common
|
ui.pens.solid ui.theme ui.tools.browser ui.tools.common
|
||||||
ui.tools.debugger ui.tools.error-list
|
ui.tools.debugger ui.tools.error-list
|
||||||
ui.tools.listener.completion ui.tools.listener.history
|
ui.tools.listener.completion ui.tools.listener.history
|
||||||
ui.tools.listener.popups vocabs vocabs.loader vocabs.parser
|
ui.tools.listener.popups vocabs vocabs.loader vocabs.parser
|
||||||
|
@ -480,9 +480,6 @@ M: listener-gadget ungraft*
|
||||||
family font-name pick set-at
|
family font-name pick set-at
|
||||||
size font-size pick set-at ;
|
size font-size pick set-at ;
|
||||||
|
|
||||||
: font-height ( font -- height )
|
|
||||||
font-metrics compute-height height>> ;
|
|
||||||
|
|
||||||
PRIVATE>
|
PRIVATE>
|
||||||
|
|
||||||
:: set-listener-font ( family size -- )
|
:: set-listener-font ( family size -- )
|
||||||
|
@ -494,6 +491,5 @@ PRIVATE>
|
||||||
clone
|
clone
|
||||||
family >>name
|
family >>name
|
||||||
size >>size
|
size >>size
|
||||||
] change-font
|
] change-font f >>line-height drop
|
||||||
font>> font-height inter line-height<<
|
|
||||||
ostream output-stream set ;
|
ostream output-stream set ;
|
||||||
|
|
Loading…
Reference in New Issue