steve
/
factor
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

ui.gadgets.editors: remove extra spaces.

char-rename
John Benediktsson 2016-08-21 21:41:08 -07:00
parent 16381beddc
commit 7a4e345f6c
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
basis/ui/gadgets/editors/editors.factor
View File

@ -224,23 +224,23 @@ M: editor draw-gadget*
[ min-rows>> [ 0 ] unless* ] [ min-rows>> [ 0 ] unless* ]
[ min-cols>> [ 0 ] unless* ] bi [ min-cols>> [ 0 ] unless* ] bi
row,col-dim ; row,col-dim ;
: max-dim ( font editor -- dim ) : max-dim ( font editor -- dim )
! hopefully no one goes over 5000 ! hopefully no one goes over 5000
[ max-rows>> [ 5000 ] unless* ] [ max-rows>> [ 5000 ] unless* ]
[ max-cols>> [ 5000 ] unless* ] bi [ max-cols>> [ 5000 ] unless* ] bi
row,col-dim ; row,col-dim ;
: txt-dim ( font editor -- dim ) : txt-dim ( font editor -- dim )
control-value text-dim ; control-value text-dim ;
PRIVATE> PRIVATE>
: editor-constrained-dim ( editor -- dim ) : editor-constrained-dim ( editor -- dim )
[ font>> ] keep [ font>> ] keep
[ max-dim ] [ max-dim ]
[ txt-dim ] [ txt-dim ]
[ min-dim ] [ min-dim ]
2tri vmax vmin { 1 0 } v+ ; 2tri vmax vmin { 1 0 } v+ ;
M: editor pref-dim* M: editor pref-dim*