Cairn.Frame
lean/Cairn/Frame.lean
What crosses the boundary each frame, before encoding. Cairn.Frame.Encode turns it into
bytes (see docs/frame.md).
Imports Cairn.UI.Node, Cairn.Input, Cairn.Surface
Structures 7
AxNode : Type
control : Option ControlRef
role : Role
rect : Rect
label : Stringvalue : Stringparent : Option NatIndex of the parent in the frame's ax array; roots have none.
focused : Boolselected : Boolchecked : Option Boolsecure : BoolA secure field (FieldView.secure): the host shows an AXSecureTextField and exposes
no value (value is empty).
TextInput : Type
Everything NSTextInputClient may ask about the focused field, answered without Lean.
control : ControlRef
rect : Rect
caret : Rect
text : Stringselection : Nat × Nat
marked : Option (Nat × Nat)
textOrigin : Point
The left end of the text's baseline, in window coordinates, after any horizontal scroll: where scalar 0 starts.
secure : BoolThe field is secure (FieldView.secure): text is bullets, and the host turns on secure
event input while it has focus.
Canvas : Type
What one Metal surface (the window, a panel) shows: M1's frame without the app-wide parts.
MenuRecord : Type
One MenuItem, flattened (Frame.ofMenu): parents come before their children, and
parent is the index of the enclosing submenu's record.
kind : MenuKind
label : Stringcontrol : Option ControlRef
The item's control (item only).
place : Option ClaimId
The submenu's place claim (submenu only, when it has one).
parent : Option Natenabled : Boolchecked : Option Boolshortcut : Option Shortcut
StatusFrame : Type
What a status item shows: its button and its menu.
SurfaceFrame : Type
One surface's record. Fields a kind doesn't use stay at their defaults: a window has no anchor or status, a status item no canvas, a hidden surface neither.
kind : SurfaceKind
place : ClaimId
shown : Booltitle : StringThe window's title.
anchor : Anchor
A panel's placement.
screen : ScreenChoice
minSize : Size
The window's smallest content size (App.minSize); 0 × 0 for other kinds.
canvas : Canvas
A window's or panel's content. A panel's size is Lean's: its width and laid-out
height.
status : StatusFrame
A status item's button and menu. For the window, the control menu open now (UI.menu):
control its owner and menu its records, no records when none is open. For the menu bar
(Surface.menuBar), its items in menu.
Frame : Type
One frame: every surface of the app, in the app's order, then what is the app's as a whole.
surfaces : Array SurfaceFrame
effects : Array Effect
subs : Array SubCmd
Subscriptions to start and stop, in order (docs/effects.md).
wake : Option NatThe earliest timer deadline, in the host's monotonic milliseconds: the host sends a
clock event no later than this.
Inductive types 3
Draw : Type
text (origin : Point) (font : Font) (color : Color) (s : String) : Draw
origin is the left end of the baseline.
popClip : Draw
shape (r : Rect) (fill : Option Color) (radius : Nat) (border : Option Border) (corner : Corner) (shadow : Option Shadow) : Draw
A rounded rect with what rect lacks: continuous corners and a soft shadow painted under
it (Style.corner, Style.shadow).
paint (r : Rect) (p : Paint) : Draw
Host-drawn pixels inside r (Style.paint).
image (r dest : Rect) (source : String) : Draw
The image the host holds for source, scaled to dest and painted only inside r
(Style.image; dest is Frame.imageDest's). Nothing if the host holds no image for it.
MenuKind : Type
The kind of a menu record: MenuItem's constructors.
SurfaceKind : Type
Definitions 8
empty : Canvas
single (c : Canvas) (effects : Array Effect := #[]) (subs : Array SubCmd := #[]) (wake : Option Nat := none) : Frame
A frame with one window (place 0) showing c: M1's frame.
window (f : Frame) : Canvas
The first window's canvas; empty when the frame has no window.
size (f : Frame) : Size
draws (f : Frame) : Array Draw
ax (f : Frame) : Array AxNode
textInput (f : Frame) : Option TextInput
cursor (f : Frame) : Cursor
Instances 25
instReprDraw : Repr Draw
instBEqDraw : BEq Draw
instInhabitedDraw : Inhabited Draw
instBEqAxNode : BEq AxNode
instReprAxNode : Repr AxNode
instInhabitedAxNode : Inhabited AxNode
instInhabitedTextInput : Inhabited TextInput
instReprTextInput : Repr TextInput
instBEqTextInput : BEq TextInput
instReprCanvas : Repr Canvas
instInhabitedCanvas : Inhabited Canvas
instDecidableEqMenuKind : DecidableEq MenuKind
instInhabitedMenuKind : Inhabited MenuKind
instReprMenuKind : Repr MenuKind
instInhabitedMenuRecord : Inhabited MenuRecord
instReprMenuRecord : Repr MenuRecord
instInhabitedStatusFrame : Inhabited StatusFrame
instReprStatusFrame : Repr StatusFrame
instInhabitedSurfaceKind : Inhabited SurfaceKind
instDecidableEqSurfaceKind : DecidableEq SurfaceKind
instReprSurfaceKind : Repr SurfaceKind
instInhabitedSurfaceFrame : Inhabited SurfaceFrame
instReprSurfaceFrame : Repr SurfaceFrame
instReprFrame : Repr Frame
instInhabitedFrame : Inhabited Frame