Cairn.App
lean/Cairn/App.lean
An app is its state, its surfaces, and its moves. The runtime (Cairn.Runtime) owns
interaction state (hover, press, focus, window size), turns events into actions by hit testing
the laid-out frame or checking the menu, and calls update.
Imports Cairn.UI.Node, Cairn.Input, Cairn.Claim, Cairn.Surface, Cairn.Font
Structures 2
UI : Type
Interaction state the runtime owns and the view may read (hover reveals, focus rings).
size : Size
hover : Option ControlRef
pressed : Option ControlRef
focus : Option ControlRef
windowFocused : Boolscroll : List (ControlRef × Int)
The offset of each scroll box that has scrolled, by its Style.scrollRef. The runtime
moves them (the wheel, the trackpad, the page keys, Tab into a box) and clamps them to the box's
content; the view reads them with scrollOf (docs/runtime.md, "Scrolling").
lists : List (ControlRef × VList.Known)
What the runtime knows of each virtual list on screen, by its scrollRef: the heights of
the rows it has laid, and the anchor (docs/runtime.md, "Virtual lists"). The runtime records
them after every layout; VList.node reads them.
kept : List (ControlRef × Int)
The offsets of scroll boxes that are not on screen and that the app keeps
(App.keepScroll), as they were when they left: the view reads them with scrollOf when the
box comes back (docs/runtime.md, "Scrolling").
keptLists : List (ControlRef × VList.Known)
What the runtime knew of each virtual list not on screen that the app keeps, likewise.
App (S : Type) : Type
init : S
surfaces : List (Surface S)
What the app shows: at most one window (a later window is ignored), panels and status items. An app with no window is an accessory app (no Dock icon, no main menu).
update : S × List Effect
A person's moves: every action names a control on screen.
receive : S × List Effect
The outside world: the clock, timers, replies and subscription events (docs/effects.md). Ignored by default.
subscriptions : List Sub
The outside inputs the app wants in this state. The runtime diffs them after every delivery and starts and stops subscriptions to match.
initEffects : List Effect
Effects to run once, when the first clock arrives (so timers start from a real time).
claims : List ClaimInfo
Every claim the app makes, from the claim commands.
initFocus : Option ControlRef
The control that has keyboard focus at launch, if it is focusable there.
maxInFlight : NatHow many requests of capped kinds (Request.Kind.capped: http, upload, loadImage)
may be with the host at once (at least 1). The runtime queues the rest (docs/effects.md,
"Requests in flight").
minSize : Size
The window's smallest content size in this state, in points. The host keeps the window
at least this big, so a person can't drag it smaller (NSWindow.contentMinSize; trusted,
^1010), and the view can be proved good at every size from it up (with Grid.minBox, for
instance). 0 × 0, no minimum, by default.
keepScroll : List ControlRef
The scroll boxes and virtual lists (by Style.scrollRef) whose offset, and what the
runtime knows of their rows, outlive their leaving the view in this state: a list on a tab not
shown comes back where it was. Any other box's offset is forgotten when it leaves the tree
(docs/runtime.md, "Scrolling"). None by default.
Inductive types 1
Surface (S : Type) : Type
One thing an app shows (docs/surfaces.md). An app declares a fixed list of them; whether
each is shown, and what it shows, is a function of the state. place is the surface's place
claim: its durable identity on the wire, in the map and in the debug socket.
window {S : Type} (place : ClaimId) (title : String) (view : S → UI → Node) :
Surface SM1's window: Metal content laid out at the window's size, with input.
panel {S : Type} (place : ClaimId)
(view : TextMetrics → S → Option PanelView) : Surface SA non-activating, click-through overlay panel; none hides it. It takes no input, so its
view doesn't read UI. The view is given the text metrics the panel is laid out with, so it
can measure content (Cairn.Layout.measure), for instance to animate between two heights.
statusItem {S : Type} (place : ClaimId) (view : S → Option StatusItem) :
Surface SA menu bar status item and its native menu; none removes it from the menu bar.
Definitions 10
listOf (ui : UI) (r : ControlRef) : VList.Known
What the runtime knows of the virtual list r: nothing until it has been laid. A list the
app keeps (App.keepScroll) is known while it is not on screen too.
scrollOf (ui : UI) (r : ControlRef) : Int
The runtime's offset for the scroll box r: 0 until it has scrolled. A box the app keeps
(App.keepScroll) keeps its offset while it is not on screen.
scrolling (ui : UI) (r : ControlRef) (st : Style) : Style
st as the scroll box r whose offset the runtime owns: scrolled by ui.scrollOf r.
example : (({} : UI).scrolling ⟨14, 0⟩ {}).scroll = some 0 := rfl
place {S : Type} : Surface S → ClaimId
comap {S T : Type} (f : T → S) : Surface S → Surface TThe same surface over a bigger state (Cairn.Runtime.logged wraps an app's state).
firstWindow {S : Type} :
List (Surface S) → Option (ClaimId × String × (S → UI → Node))The first window in a surface list: its place, title and view.
emptyView : Node
What an app with no window lays out as its window: nothing.
view {S : Type} (app : App S) : S → UI → Node
windowPlace {S : Type} (app : App S) : Option ClaimIdThe window's place claim, if the app has a window. Bare surface-local events (M1's) go to this window.
accessory {S : Type} (app : App S) : BoolAn app with no window runs as an accessory (docs/surfaces.md, section 3).
Theorems 3
place_comap {S T : Type} (f : T → S) (x : Surface S) :
(comap f x).place = x.place
firstWindow_comap {S T : Type} (f : T → S) (xs : List (Surface S)) :
firstWindow (List.map (Surface.comap f) xs) =
Option.map
(fun x =>
match x with
| (p, t, v) => (p, t, fun s ui => v (f s) ui))
(firstWindow xs)
view_comap {S : Type} (app : App S) {T : Type} (f : T → S) (b : App T)
(h : b.surfaces = List.map (Surface.comap f) app.surfaces) (s : T) (ui : UI) :
b.view s ui = app.view (f s) uiThe view of an app whose surfaces are app's over a bigger state reads the smaller one.
Instances 3
instInhabitedUI : Inhabited UI
instReprUI : Repr UI
instDecidableEqUI : DecidableEq UI