Cairn.Frame.Build
lean/Cairn/Frame/Build.lean
Frame.ofLaid: a laid-out tree becomes what crosses the boundary: draw commands in paint
order, the accessibility tree, and the focused field's text-input state.
- Paint order (back to front, depth first). A box paints its background and border (one
rect, only when it has either), then its children, wrapped inpushClip/popClipof its rect when it clips (Style.clips:clip, or a scroll box). A scroll box paints only the children whose visible part (rect ∩ clip) is non-empty; the rest are scrolled out of view. Text paints onetextat its baseline origin. A field paints its background and border, then, clipped to its rect, its selection rects, its text (or its placeholder at half alpha when the text is empty), and its caret when focused and the selection is empty. - Accessibility. One
AxNodeper control (boxes with a control, fields) and per text, in paint order, each with its visible rect (rect ∩ clip). A scroll box without a control has a node of its own, rolescrollArea, and is its children's parent; a node's parent is the nearest enclosing control or scroll box. Every control has its node even when it is scrolled out of view (its rect is then empty); the host leaves those out of what it exposes (docs/trusted.md). A field's value is its text and its role istextField; a secure field's node is markedsecureand has no value. - Text input describes the first field whose control has focus.
Focus comes from the runtime (UI.focus), the one source of truth; FieldView.focused is for the
view's own styling and is not read here. Laid.text's baseline is absolute (window y). Laid.controls is layout's (Layout/Facts.lean).
controls_ofLaid_layout, which composes controls_ofLaid with layout, is in Frame/Layout.lean.
Theorems: controls_ofLaid (the accessibility tree's controls are exactly the laid tree's, in
order, which is how presence reaches the accessibility mirror), mem_ax_ofLaid,
ax_refs_nodup (distinct refs in the tree give distinct refs in the mirror), parent_lt_ofLaid
(every parent index points at an earlier node) and balanced_ofLaid (clips are balanced).
Imports Cairn.Frame, Cairn.App, Cairn.Layout.Facts
Definitions 19
selectionColor : Color
Selection highlight: the macOS accent blue at 30%.
imageDest (r : Rect) (f : ImageFill) : Rect
Where an image of f.width×f.height pixels is painted for the box r, in logical points:
the box itself for fill (or when either has no area); for contain the largest rect of the
image's aspect ratio inside the box, and for cover the smallest one covering it, centred.
Lengths are rounded down for contain and up for cover, so contain never spills out of the
box and cover never leaves a gap (imageDest_contain_inside, imageDest_cover_covers).
boxDraws (r : Rect) (s : Style) : List Draw
A box's own paint: its background and border (one rect, or one shape when it has a
shadow or continuous corners), then its host-drawn pixels, then its image.
halfAlpha (c : Color) : Color
fieldDraws (focus : Option ControlRef) (ts : TextStyle) (c : Control) (v : FieldView) (origin : Point) (caret : Rect) (sel : List Rect) : List Draw
What a field paints inside its clip.
paint (focus : Option ControlRef) : Laid → List Draw
Draw commands for a laid tree, back to front.
paintAll (focus : Option ControlRef) (scrolled : Bool) : List Laid → List Draw
Draw commands for a box's children, back to front. In a scroll box (scrolled), a child
whose visible part is empty paints nothing.
controlNode (focus : Option ControlRef) (parent : Option Nat) (rect : Rect) (c : Control) : AxNode
scrollNode (parent : Option Nat) (rect : Rect) : AxNode
A scroll box's own node.
axOf (focus : Option ControlRef) (parent : Option Nat) (acc : Array AxNode) : Laid → Array AxNode
Append the accessibility nodes of a laid tree to acc; parent is the index of the
nearest enclosing control's or scroll box's node.
axAll (focus : Option ControlRef) (parent : Option Nat) (acc : Array AxNode) : List Laid → Array AxNode
textInputOf (focus : Option ControlRef) : Laid → Option TextInput
The text-input state of the first focused field.
textInputAll (focus : Option ControlRef) : List Laid → Option TextInput
ofLaid (ui : UI) (l : Laid) : Canvas
The canvas for a laid tree. The runtime fills in cursor.
ParentsOk (ax : Array AxNode) : Prop
Every node's parent is an earlier node.
ParentBelow (parent : Option Nat) (n : Nat) : Prop
clipDepth : Nat → List Draw → Option Nat
The clip stack depth after running ds from depth d; none if a popClip finds the
stack empty.
Balanced (ds : List Draw) : Prop
Every popClip closes an earlier pushClip, and every pushClip is closed.
NoClip (ds : List Draw) : Prop
Draws with no clip commands leave the depth alone.
Theorems 20
imageDest_contain_inside (r : Rect) (f : ImageFill) (hf : f.fit = Fit.contain) : have d := imageDest r f; r.x ≤ d.x ∧ d.x + d.w ≤ r.x + r.w ∧ r.y ≤ d.y ∧ d.y + d.h ≤ r.y + r.h
contain stays inside the box.
imageDest_cover_covers (r : Rect) (f : ImageFill) (hf : f.fit = Fit.cover) : have d := imageDest r f; d.x ≤ r.x ∧ r.x + r.w ≤ d.x + d.w ∧ d.y ≤ r.y ∧ r.y + r.h ≤ d.y + d.h
cover leaves no part of the box uncovered.
axOf_controls (focus : Option ControlRef) (parent : Option Nat) (acc : Array AxNode) (l : Laid) : List.filterMap AxNode.control (axOf focus parent acc l).toList = List.filterMap AxNode.control acc.toList ++ List.map Control.ref l.controls
axAll_controls (focus : Option ControlRef) (parent : Option Nat) (acc : Array AxNode) (ls : List Laid) : List.filterMap AxNode.control (axAll focus parent acc ls).toList = List.filterMap AxNode.control acc.toList ++ List.map Control.ref (Laid.controlsList ls)
controls_ofLaid (ui : UI) (l : Laid) : List.filterMap AxNode.control (ofLaid ui l).ax.toList = List.map Control.ref l.controls
Presence reaches accessibility. The controls in the frame's accessibility tree are exactly the controls of the laid tree, in order.
mem_ax_ofLaid (ui : UI) (l : Laid) (c : ControlRef) : (∃ n, n ∈ (ofLaid ui l).ax ∧ n.control = some c) ↔ ∃ k, k ∈ l.controls ∧ k.ref = c
A claim's control is in the accessibility tree iff it is in the laid tree.
ax_refs_nodup (ui : UI) (l : Laid) (h : (List.map Control.ref l.controls).Nodup) : (List.filterMap AxNode.control (ofLaid ui l).ax.toList).Nodup
One node per control. If the laid tree's controls have pairwise distinct refs (an app
invariant), so do the accessibility nodes': the host may key its elements by ControlRef.
push {ax : Array AxNode} {n : AxNode} (h : ParentsOk ax)
(hn : ParentBelow n.parent ax.size) : ParentsOk (ax.push n)
axOf_size (focus : Option ControlRef) (parent : Option Nat) (acc : Array AxNode) (l : Laid) : acc.size ≤ (axOf focus parent acc l).size
axAll_size (focus : Option ControlRef) (parent : Option Nat) (acc : Array AxNode) (ls : List Laid) : acc.size ≤ (axAll focus parent acc ls).size
mono {p : Option Nat} {n m : Nat} (h : ParentBelow p n)
(hm : n ≤ m) : ParentBelow p m
axOf_parents (focus : Option ControlRef) (parent : Option Nat) (acc : Array AxNode) (l : Laid) (h : ParentsOk acc) (hp : ParentBelow parent acc.size) : ParentsOk (axOf focus parent acc l)
axAll_parents (focus : Option ControlRef) (parent : Option Nat) (acc : Array AxNode) (ls : List Laid) (h : ParentsOk acc) (hp : ParentBelow parent acc.size) : ParentsOk (axAll focus parent acc ls)
parent_lt_ofLaid (ui : UI) (l : Laid) : ParentsOk (ofLaid ui l).ax
Every accessibility node's parent comes before it, so the host can build the tree in one pass.
clipDepth_noClip {ds : List Draw} (h : NoClip ds) (d : Nat) (rest : List Draw) :
clipDepth d (ds ++ rest) = clipDepth d rest
noClip_boxDraws (r : Rect) (s : Style) : NoClip (boxDraws r s)
noClip_fieldDraws (focus : Option ControlRef) (ts : TextStyle) (c : Control) (v : FieldView) (o : Point) (caret : Rect) (sel : List Rect) : NoClip (fieldDraws focus ts c v o caret sel)
clipDepth_paint (focus : Option ControlRef) (l : Laid) (d : Nat) (rest : List Draw) : clipDepth d (paint focus l ++ rest) = clipDepth d rest
clipDepth_paintAll (focus : Option ControlRef) (sc : Bool) (ls : List Laid) (d : Nat) (rest : List Draw) : clipDepth d (paintAll focus sc ls ++ rest) = clipDepth d rest
balanced_ofLaid (ui : UI) (l : Laid) : Balanced (ofLaid ui l).draws.toList
Clips are balanced in every frame ofLaid builds.