ui.tools.listener: update interactor's line-height in set-listener-font

factor-shell
Alexander Iljin 2017-10-13 20:27:08 +03:00 committed by John Benediktsson
parent dc001f9a34
commit 6de6cb687f
1 changed files with 22 additions and 15 deletions

View File

@ -1,19 +1,21 @@
! Copyright (C) 2005, 2010 Slava Pestov. ! Copyright (C) 2005, 2010 Slava Pestov.
! See http://factorcode.org/license.txt for BSD license. ! See http://factorcode.org/license.txt for BSD license.
USING: accessors arrays assocs calendar combinators USING: accessors arrays assocs calendar combinators
combinators.short-circuit concurrency.flags concurrency.mailboxes combinators.short-circuit concurrency.flags
continuations destructors documents documents.elements fonts fry concurrency.mailboxes continuations destructors documents
hashtables help help.markup help.tips io io.styles kernel lexer documents.elements fonts fry hashtables help help.markup
listener literals locals math math.vectors models models.arrow help.tips io io.styles kernel lexer listener literals locals
models.delay namespaces parser prettyprint sequences math math.vectors models models.arrow models.delay namespaces
source-files.errors strings system threads tools.errors.model ui parser prettyprint sequences source-files.errors strings system
ui.commands ui.gadgets ui.gadgets.editors ui.gadgets.glass threads tools.errors.model ui ui.commands ui.gadgets
ui.gadgets.labeled ui.gadgets.panes ui.gadgets.scrollers ui.gadgets.editors ui.gadgets.glass ui.gadgets.labeled
ui.gadgets.status-bar ui.gadgets.toolbar ui.gadgets.tracks ui.gestures ui.gadgets.panes ui.gadgets.scrollers ui.gadgets.status-bar
ui.operations ui.pens.solid ui.theme ui.tools.browser ui.tools.common ui.gadgets.toolbar ui.gadgets.tracks ui.gestures ui.operations
ui.tools.debugger ui.tools.error-list ui.tools.listener.completion ui.pens.solid ui.text ui.theme ui.tools.browser ui.tools.common
ui.tools.listener.history ui.tools.listener.popups vocabs ui.tools.debugger ui.tools.error-list
vocabs.loader vocabs.parser vocabs.refresh words ; ui.tools.listener.completion ui.tools.listener.history
ui.tools.listener.popups vocabs vocabs.loader vocabs.parser
vocabs.refresh words ;
IN: ui.tools.listener IN: ui.tools.listener
TUPLE: interactor < source-editor TUPLE: interactor < source-editor
@ -478,6 +480,9 @@ 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 -- )
@ -485,8 +490,10 @@ PRIVATE>
family size make-font-style family size make-font-style
inter output>> make-span-stream :> ostream inter output>> make-span-stream :> ostream
ostream inter output<< ostream inter output<<
inter font>> clone inter [
clone
family >>name family >>name
size >>size size >>size
inter font<< ] change-font
font>> font-height inter line-height<<
ostream output-stream set ; ostream output-stream set ;