Cairn.Layout.Core
lean/Cairn/Layout/Core.lean
Layout
layout m window node turns a Node into a Laid: every rect, clip, baseline, caret and
selection resolved in integer logical points. It is total and pure, and works in two passes:
- Measure (
measure, bottom-up): each node's preferred ("hug") size, stored in aSizedtree so that no subtree is measured twice. It is passed the width the parent offers, which only wrapped text (Node.para) uses: a para measures into a clipping column of its lines, onetexteach (paraLines), soarrangenever sees a para. - Arrange (
arrange, top-down): each node is given a rect by its parent and places its children inside its content box.
The semantics are specified in docs/layout.md; the theorems are in Cairn.Layout.Proofs.
Every definition here is plain structural recursion over lists so that the proofs can follow
the code.
Imports Cairn.UI.Node, Cairn.Text.Wrap
Structures 2
Item : Type
What a parent needs to know about a child to place it.
Line : Type
Everything a line of children shares.
horiz : Boolalign : Align
c0 : IntCross-axis start and length of the content box.
cc : IntL : IntLeftover space for fill children, and how many there are.
f : Natspacing : IntSpace after the i-th child.
Inductive types 1
Sized : Type
A node with its preferred size resolved. This is the measure pass's output and the arrange
pass's input. size is the size the node asks for: fixed n gives n, hug and fill give
the intrinsic size of the content plus padding, floored at zero.
Definitions 51
size : Sized → Size
sizings : Sized → Sizing × Sizing
Sizing on each axis (text always hugs).
item (s : Sized) : Item
resolve (s : Sizing) (intrinsic : Int) : Int
Resolve a preferred length: fixed n is n; hug and fill are the intrinsic length,
floored at zero.
gaps (gap k : Nat) : Int
Total length of the gaps between k children.
maxAll : List Int → Int
Largest element, or 0.
contentSize (axis : Axis) (gap : Nat) (kids : List Size) : Size
Intrinsic content size of a container from its children's preferred sizes.
shown (v : FieldView) : String
The string a field sizes itself to: its text, or its placeholder when empty.
offAt (offs : Array Int) (i : Nat) : Int
Caret offset at scalar index i, clamped to the end of the text.
innerAvail (st : Style) (aw : Int) : Int
The width a box offers its children to wrap in: its own (fixed) width or the width it was
offered, less its horizontal padding.
wrapWidth (wr : Wrap) (aw : Int) : Int
The width a wrapped text breaks at: its fixed width, or the width it was offered.
paraStyle (wr : Wrap) : Style
A wrapped text is laid out as a column of its lines that clips to its rect.
paraLines (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) : List Sized
The lines of a wrapped text, each a text sized to its width by the line height. The
offsets come from one measurement of the whole string.
measure (m : TextMetrics) (aw : Int) : Node → Sized
The measure pass. aw is the width the parent offers, which only wrapped text uses.
measureList (m : TextMetrics) (aw : Int) : List Node → List Sized
isFill : Sizing → Bool
mainBase (s : Sizing) (pref : Int) : Int
Main-axis length a child asks for before leftover space is shared: fill asks for 0.
crossPlace (al : Align) (c0 cc : Int) (s : Sizing) (pref : Int) (stretch : Bool) : Int × Int
Cross-axis placement within [c0, c0 + cc): returns position and length.
mainSizing (horiz : Bool) (it : Item) : Sizing
crossSizing (horiz : Bool) (it : Item) : Sizing
mainPref (horiz : Bool) (it : Item) : Int
crossPref (horiz : Bool) (it : Item) : Int
mainSize (horiz : Bool) (L : Int) (f j : Nat) (it : Item) : Int
The main-axis length of an item, given the shared leftover L among f fill children, j
of which come before it.
mkRect (horiz : Bool) (mainPos mainLen crossPos crossLen : Int) : Rect
go (ln : Line) : Nat → Nat → Int → List Item → List Rect
Place a line of children: i is the child's index, j the number of fill children before
it, pos where it starts on the main axis.
spacing (justify : Align) (gap : Nat) (free : Int) (k i : Nat) : Int
Space after child i for justify: gap, plus for stretch (space-between) an equal
share of the free space when there is some and more than one child.
startOffset (justify : Align) (free : Int) : Int
Where the first child starts, relative to the content box, for justify.
mainOf (horiz : Bool) (r : Rect) : Int
The main-axis length of a row (horiz) or column's content box.
baseSum (horiz : Bool) (items : List Item) : Int
Sum of the children's base lengths (fill children count 0).
fillCount (horiz : Bool) (items : List Item) : Nat
Number of fill children on the main axis.
leftover (horiz : Bool) (st : Style) (content : Rect) (items : List Item) : Int
Leftover main-axis space shared by fill children, floored at zero.
free (horiz : Bool) (st : Style) (content : Rect) (items : List Item) : Int
Main-axis space left after every child and gap; this is what justify distributes.
With fill children the line is full unless it overflows.
lineOf (horiz : Bool) (st : Style) (content : Rect) (items : List Item) : Line
lineRects (horiz : Bool) (st : Style) (content : Rect) (items : List Item) : List Rect
Rects for the children of a row (horiz) or column with content box content.
stackRects (st : Style) (content : Rect) (items : List Item) : List Rect
Rects for the children of a stack: each child is placed in the whole content box,
horizontally by justify and vertically by align.
placeRects (st : Style) (r : Rect) (items : List Item) : List Rect
Rects for a container's children before any scrolling, given the container's rect.
horiz : Axis → Bool
Whether an axis runs horizontally (rows) or vertically (columns and stacks).
scrollBy (horiz : Bool) (o : Int) (q : Rect) : Rect
q moved back by o points along an axis: left when horiz, otherwise up.
clips (st : Style) : Bool
Whether a box clips its children: when it says so, and always when it scrolls.
scrolled (st : Style) (rs : List Rect) : List Rect
Children's rects moved by a scroll box's offset; unchanged in any other box.
childRects (st : Style) (r : Rect) (items : List Item) : List Rect
Rects for a container's children, given the container's rect: placed as its axis says, then,
in a scroll box (scroll = some o), moved back by o along that axis (a row scrolls
horizontally, a column or stack vertically).
scrollFor (co cw : Int) : Int
How far a field's text is scrolled left so that a caret at offset co is visible in a
content box cw wide: zero unless the caret would fall off the right edge, and then just
enough to put it at the right edge.
field (m : TextMetrics) (clip r : Rect) (st : Style) (ts : TextStyle) (ctl : Control) (v : FieldView) : Laid
Lay out a field in r: text vertically centred in the content box, scrolled horizontally
so the caret is visible.
innerClip (st : Style) (clip r : Rect) : Rect
Region a container's children may paint in: its own clip, intersected with its rect when
it clips (Style.clips: a scroll box always does).
arrange (m : TextMetrics) (clip r : Rect) : Sized → Laid
The arrange pass: lay out s in r, painting within clip.
arrangeList (m : TextMetrics) (clip : Rect) : List Rect → List Sized → List Laid
Arrange children against their rects (the lists always have the same length; a missing rect would be empty).
windowRect (w : Size) : Rect
The window as a rect at the origin, sizes floored at zero.
rootRect (window : Size) (s : Sized) : Rect
The root's rect: at the origin, fill takes the window's length, otherwise the preferred
length.
layout (m : TextMetrics) (window : Size) (n : Node) : Laid
Lay out a view in a window.
Instances 1
instInhabitedSized : Inhabited Sized