From fdcbf0d11004561e0b25b90c6359a0a3f774955c Mon Sep 17 00:00:00 2001 From: John Benediktsson Date: Mon, 22 Aug 2016 07:52:47 -0700 Subject: [PATCH] Revert "ui.gadgets.editors: remove extra spaces." This reverts commit 7a4e345f6c199b8ddfb7faec2121a2dc80ab1da6. --- basis/ui/gadgets/editors/editors.factor | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/basis/ui/gadgets/editors/editors.factor b/basis/ui/gadgets/editors/editors.factor index 37350b3830..e1119af718 100644 --- a/basis/ui/gadgets/editors/editors.factor +++ b/basis/ui/gadgets/editors/editors.factor @@ -224,23 +224,23 @@ M: editor draw-gadget* [ min-rows>> [ 0 ] unless* ] [ min-cols>> [ 0 ] unless* ] bi row,col-dim ; - + : max-dim ( font editor -- dim ) ! hopefully no one goes over 5000 [ max-rows>> [ 5000 ] unless* ] [ max-cols>> [ 5000 ] unless* ] bi row,col-dim ; - + : txt-dim ( font editor -- dim ) control-value text-dim ; - + PRIVATE> : editor-constrained-dim ( editor -- dim ) [ font>> ] keep [ max-dim ] [ txt-dim ] - [ min-dim ] + [ min-dim ] 2tri vmax vmin { 1 0 } v+ ; M: editor pref-dim* -- 2.34.1