Cairn.UI.Node
lean/Cairn/UI/Node.lean
What view returns (Node) and what layout produces (Laid).
A Node says what is on screen and how it wants to be sized; layout turns it into a Laid
with every rect and clip resolved. A node that performs a move carries a Control naming the
claim, which is how presence, pressability and the accessibility mirror find it.
Imports Cairn.Geometry, Cairn.Claim, Cairn.Font, Cairn.Effects, Cairn.Input
Structures 17
Color : Type
r : UInt8g : UInt8b : UInt8a : UInt8Border : Type
width : Natcolor : Color
Shadow : Type
A soft shadow under a box's shape, as SwiftUI's shadow(color:radius:x:y:): the shape's
silhouette in color, blurred by radius points and moved by (x, y). With no offset it is a
glow.
Paint : Type
Pixels the host draws: the shader registered under shader fills the box, fed with these
numbers (what they mean is the shader's contract) and with the host's clock, as milliseconds
since origin (a time on the runtime's monotonic clock), so it can move between frames.
shader : Stringorigin : Natscalars : List Intarrays : List (List Int)ImageFill : Type
Host-drawn pixels from a loaded image: the host paints the image it holds for source into
the box as fit says. width and height are its size in pixels, as the load answered
(Reply.image); Lean places it from them (Frame.imageDest), so the host only scales.
Row : Type
A row whose height is known: it was laid at that height.
index : NatIts place in the list's keys.
key : Natheight : NatIts height as laid, at least one point.
Anchor : Type
The row the reader is at: the first row showing at the offset offset, whose top in the
list's content was top in the heights it was recorded with. A row the clamp kept from its
place within a batch is held: the place to keep it at is hold points below where it is
(VList.anchorAt), until the batch's frame is shown (Known.letGo).
key : Nattop : Intoffset : Inthold : IntKnown : Type
What the runtime knows of one list (UI.lists), recorded after every layout: the heights of
the rows it has laid, sorted by index, at the width they were laid at; the box's length; and
the anchor.
width : IntThe width the rows were laid at: a different width forgets every height.
count : NatThe number of rows when they were recorded.
rows : Array Row
viewport : IntThe box's length the last time it was laid; 0 before then.
anchor : Option Anchor
est : NatThe estimate for the rows not yet laid: the mean of the first heights recorded at this width, kept until the width changes, so that recording more heights doesn't move every row below them; 0 before any.
Info : Type
What a laid virtual list says of itself (Style.rows), for the runtime to record and the
fuzzer to check: what the view read, the heights it laid out by, and the window it laid.
model : Array Row
The known heights for these keys (VList.model): known.rows moved to the keys' indices.
keys : Array Natestimate : Option NatThe estimate the view was given, if any, and the one it used.
est : Natoverscan : Natviewport : Intfirst : NatThe rows laid: indices [first, last).
last : NatControl : Type
A node that performs a move.
ref : ControlRef
role : Role
label : Stringvalue : Stringchecked : Option Boolselected : Boolappear : BoolTell the app when this control comes on screen: the runtime delivers Action.appear when
it has a visible part at the end of a batch and didn't at the end of the last one (or wasn't
in the tree). How an app hears that the end of a list is in view (docs/runtime.md, "Appear").
Shortcut : Type
A keyboard shortcut shown on a menu item (⌘Q). A status item's and a control's menu honour it
only while open; an item in the app's menu bar (Surface.menuBar) has it whenever the app is
active (a key equivalent).
ControlMenu : Type
A control's menu (docs/surfaces.md, "Menus on controls"): a native menu the runtime opens
over the control, built like a status item's. The secondary click on the control (or on anything
inside it that has no menu of its own), the context-menu key (Shift-F10) while it has focus and
VoiceOver's Show Menu open it; with button, the control is a menu button (⋯) and a primary
click, Space or Return open it too, instead of pressing it. Choosing an item is a press of that
item's control (Event.menuSelect with the window's place); opening and closing reach no
update. A menu with no items is no menu.
items : List MenuItem
button : BoolStyle : Type
axis : Axis
width : Sizing
height : Sizing
padding : Insets
gap : Natalign : Align
Cross-axis alignment of children.
justify : Align
Main-axis placement of children when there's space left over.
background : Option Color
border : Option Border
radius : Natclip : BoolClip children to this box.
corner : Corner
shadow : Option Shadow
Painted under the box's background.
paint : Option Paint
Host-drawn pixels over the background, under the children.
image : Option ImageFill
A loaded image over the background (and the paint), under the children.
scroll : Option IntA scroll box: some o lays the children out as the box's axis says,
then moves them back by o points along that axis (up, or left in a row), and clips them to
the box. none is an ordinary box. The children keep their real rects, possibly above or
below the box; what shows is rect ∩ clip (docs/layout.md, "Scroll boxes").
scrollRef : Option ControlRef
The scroll box's identity, when the runtime owns its offset (docs/runtime.md,
"Scrolling"): the wheel, the trackpad and the page keys move it, and the view reads it back with
UI.scrollOf (UI.scrolling sets both fields). Usually a place claim's ref. A box with
scroll and no scrollRef scrolls only as far as the view says.
rows : Option VList.Info
A virtual list's box (Cairn.VList): which rows it laid and the heights it laid them
by. The runtime records the rows' real heights from it after every layout. Set by VList.node
only.
TextStyle : Type
FieldView : Type
What a text field shows. Indices are Unicode scalar positions into text. The editing
model that produces this lives in Cairn.Text.
text : Stringcaret : Natanchor : NatSelection is [min anchor caret, max anchor caret).
marked : Option (Nat × Nat)
IME composition in progress, as a range of text.
placeholder : Stringfocused : Boolsecure : BoolA secure field (a password): text is one bullet per scalar of what was typed
(Cairn.Text.SecureField.view), so it is drawn, measured and dumped as bullets; the frame
marks it so the accessibility mirror shows an AXSecureTextField with no value and the host
turns on secure event input while it has focus (docs/text.md, "Secure fields").
Wrap : Type
How a wrapped text (Node.para) is sized and broken into lines. The rules are in
docs/layout.md ("Wrapped text") and Cairn.Text.Wrap.
width : Sizing
fixed n wraps at n; hug and fill wrap at the width the parent offers. fill then
takes the parent's whole cross or leftover length; hug the widest line.
height : Sizing
hug is the lines' height (lines × line height). A shorter fixed height clips.
maxLines : Option NatKeep at most this many lines.
keep : Keep
align : Align
Where each line sits in the width: start (and stretch) left, center, finish right.
lineSpacing : NatPoints between lines (SwiftUI's lineSpacing).
Image : Type
An image on screen (Node.image): where its pixels come from (a file path, ~/ for the
home folder, or an http/https URL; the host loads it for Request.loadImage), the box it
takes in logical points, and what is known of it so far. The box is the same in every state, so
nothing moves when the pixels arrive or fail (Layout.measure_image).
source : Stringwidth : Natheight : Natstate : ImageState
fit : Fit
placeholder : Color
The box while loading.
backdrop : Option Color
Under a loaded image: what shows through its transparency and contain's bands.
failedFill : Color
The box, and the colour of its border and words, when the load failed.
failedInk : Color
Inductive types 11
Axis : Type
row and column lay children out along an axis; stack puts them on top of each other,
later children on top.
Align : Type
Sizing : Type
fill shares the parent's leftover main-axis space equally among fill children, and
takes the parent's full cross-axis size.
Corner : Type
How a rounded box's corners turn: a circular arc, or Apple's continuous curve (SwiftUI's
RoundedRectangle(style: .continuous)), which starts further along the edge and has no jump in
curvature.
Fit : Type
How an image's pixels fill its box: stretched to it (fill), scaled to fit inside it with the
aspect ratio kept (contain, centred, leaving bands), or scaled to cover it with the aspect ratio
kept (cover, centred, cut by the box).
Role : Type
MenuItem : Type
One entry of a native menu: a status item's, a control's (ControlMenu) or the app's own in
the menu bar (docs/surfaces.md). The host builds a real NSMenu from it.
item (control : Control) (enabled : Bool := true) (shortcut : Option Shortcut := none) : MenuItem
An item that performs a move. control.checked = some b makes it a checkbox item;
enabled = false greys it out (it stays in the menu, with its control).
info (label : String) : MenuItem
A line of text that does nothing: a status line, "None yet". Shown disabled.
separator : MenuItem
Keep : Type
Which lines a wrapped text keeps when it has more than maxLines: the first ones, or the
last ones (a growing transcript that shows its end).
Node : Type
Laid : Type
A laid-out node. clip is the region this node may paint in (the intersection of every
clipping ancestor), so the visible part of a node is rect.inter clip.
ImageState : Type
What an app knows of an image so far: not loaded yet, loaded (its size in pixels, from
Reply.image), or failed (from Reply.failed).
loading : ImageState
ready (width height : Nat) : ImageState
failed (fault : Fault) (message : String) : ImageState
Definitions 11
letGo (k : Known) : Known
What is known once a frame is shown: a held anchor is let go, so the row is kept where it now shows.
mark : Option ControlMenu → Option Bool
What the accessibility mirror says of a menu: some true a menu button, some false a
context menu, none no menu (or one with no items).
rect : Laid → Rect
clip : Laid → Rect
visible (l : Laid) : Rect
control? : Laid → Option Control
faultText : Fault → String
The words a failed image shows.
style (i : Image) : Style
The image's box: fixed at its size in every state, clipping; the placeholder colour while
loading, the pixels once loaded, a bordered box with the fault's words when failed.
children (i : Image) : List Node
What a failed image says, centred in its box (clipped to it); nothing otherwise.
image (i : Image) : Node
An image node. A box of the image's size whatever its state, so layout knows its size
before the pixels exist; it has no control (an image is not a move) and paints, from back to
front, its state's background, the host's pixels once loaded (Style.image), and a failure's
words.
Instances 96
instBEqColor : BEq Color
instInhabitedColor : Inhabited Color
instDecidableEqColor : DecidableEq Color
instReprColor : Repr Color
instInhabitedAxis : Inhabited Axis
instReprAxis : Repr Axis
instDecidableEqAxis : DecidableEq Axis
instBEqAxis : BEq Axis
instReprAlign : Repr Align
instDecidableEqAlign : DecidableEq Align
instInhabitedAlign : Inhabited Align
instBEqAlign : BEq Align
instDecidableEqSizing : DecidableEq Sizing
instReprSizing : Repr Sizing
instInhabitedSizing : Inhabited Sizing
instBEqSizing : BEq Sizing
instBEqBorder : BEq Border
instReprBorder : Repr Border
instDecidableEqBorder : DecidableEq Border
instInhabitedBorder : Inhabited Border
instReprCorner : Repr Corner
instBEqCorner : BEq Corner
instInhabitedCorner : Inhabited Corner
instDecidableEqCorner : DecidableEq Corner
instInhabitedShadow : Inhabited Shadow
instBEqShadow : BEq Shadow
instDecidableEqShadow : DecidableEq Shadow
instReprShadow : Repr Shadow
instBEqPaint : BEq Paint
instDecidableEqPaint : DecidableEq Paint
instReprPaint : Repr Paint
instInhabitedPaint : Inhabited Paint
instInhabitedFit : Inhabited Fit
instBEqFit : BEq Fit
instDecidableEqFit : DecidableEq Fit
instReprFit : Repr Fit
instInhabitedImageFill : Inhabited ImageFill
instBEqImageFill : BEq ImageFill
instReprImageFill : Repr ImageFill
instDecidableEqImageFill : DecidableEq ImageFill
instDecidableEqRow : DecidableEq Row
instReprRow : Repr Row
instInhabitedRow : Inhabited Row
instBEqRow : BEq Row
instDecidableEqAnchor : DecidableEq Anchor
instBEqAnchor : BEq Anchor
instInhabitedAnchor : Inhabited Anchor
instReprAnchor : Repr Anchor
instInhabitedKnown : Inhabited Known
instReprKnown : Repr Known
instBEqKnown : BEq Known
instDecidableEqKnown : DecidableEq Known
instBEqInfo : BEq Info
instReprInfo : Repr Info
instInhabitedInfo : Inhabited Info
instReprRole : Repr Role
instDecidableEqRole : DecidableEq Role
instBEqRole : BEq Role
instInhabitedRole : Inhabited Role
instInhabitedControl : Inhabited Control
instReprControl : Repr Control
instBEqControl : BEq Control
instDecidableEqShortcut : DecidableEq Shortcut
instReprShortcut : Repr Shortcut
instInhabitedShortcut : Inhabited Shortcut
instInhabitedMenuItem : Inhabited MenuItem
instReprMenuItem : Repr MenuItem
instBEqMenuItem : BEq MenuItem
instBEqControlMenu : BEq ControlMenu
instReprControlMenu : Repr ControlMenu
instInhabitedControlMenu : Inhabited ControlMenu
instReprStyle : Repr Style
instBEqStyle : BEq Style
instInhabitedStyle : Inhabited Style
instInhabitedTextStyle : Inhabited TextStyle
instBEqTextStyle : BEq TextStyle
instReprTextStyle : Repr TextStyle
instInhabitedFieldView : Inhabited FieldView
instReprFieldView : Repr FieldView
instBEqFieldView : BEq FieldView
instDecidableEqKeep : DecidableEq Keep
instBEqKeep : BEq Keep
instReprKeep : Repr Keep
instInhabitedKeep : Inhabited Keep
instReprWrap : Repr Wrap
instInhabitedWrap : Inhabited Wrap
instBEqWrap : BEq Wrap
instInhabitedNode : Inhabited Node
instReprNode : Repr Node
instInhabitedLaid : Inhabited Laid
instReprLaid : Repr Laid
instReprImageState : Repr ImageState
instInhabitedImageState : Inhabited ImageState
instDecidableEqImageState : DecidableEq ImageState
instReprImage : Repr Image
instInhabitedImage : Inhabited Image
Virtual lists: what the runtime knows of one
The data a virtual list (Cairn.VList, docs/layout.md, "Virtual lists") and the runtime pass
each other. The logic is in Cairn.VList.