Cairn.Surface
lean/Cairn/Surface.lean
What an app shows besides a window (docs/surfaces.md): a menu bar status item with its
native menu, and a non-activating, click-through overlay panel, both as data. Cairn.App
collects an app's surfaces; the runtime keeps what each one shows (Cairn.Runtime.Shown) and
the frame carries it (docs/frame.md, surface records).
The menu is a description, not a laid tree: the host builds a real NSMenu from it, and every
actionable item is a Control naming a move, so presence, enablement and checkmarks are facts
about this value (refs, enabledOf, checkedOf) with no layout in between.
MenuItem is a nested inductive, so every function over it is a structural pair (f on one
item, fs on a list), per AGENTS.md.
Imports Cairn.UI.Node, Cairn.Input
Structures 2
StatusItem : Type
A menu bar status item and its menu.
symbol : StringAn SF Symbol name, drawn as a template image so it follows the menu bar's appearance.
title : StringOptional text beside the symbol.
label : StringWhat VoiceOver says for the button.
control : ControlRef
Opening the menu is a press on this control.
PanelView : Type
What a shown panel holds. The panel's window behaviour (never key, click-through, on every Space) is fixed by the host, not chosen here (docs/surfaces.md, docs/trusted.md).
width : NatWidth in points; the height is the laid-out content's.
anchor : Anchor
screen : ScreenChoice
content : Node
Inductive types 2
Anchor : Type
Where the host puts a panel on its screen.
ScreenChoice : Type
Which screen a panel is shown on.
pointer : ScreenChoice
The screen the pointer is on when the panel is shown; it stays there until hidden.
main : ScreenChoice
Definitions 11
button (r : ControlRef) (label : String) (enabled : Bool := true) (shortcut : Option Shortcut := none) : MenuItem
A plain item for r.
check (r : ControlRef) (label : String) (on : Bool) (enabled : Bool := true) : MenuItem
A checkbox item for r, ticked when on.
refsOf : MenuItem → List ControlRef
The refs of an item's actionable items, depth first, in menu order.
refs : List MenuItem → List ControlRef
The refs of every actionable item in a menu, depth first, in menu order.
enabledRefsOf : MenuItem → List ControlRef
The refs of an item's enabled actionable items.
enabledRefs : List MenuItem → List ControlRef
The refs of every enabled actionable item in a menu, in any submenu: what a selection may
press (Cairn.Runtime.route, menuSelect).
findOf (r : ControlRef) : MenuItem → Option (Control × Bool)
The first actionable item with ref r in an item: its control and whether it is enabled.
find (r : ControlRef) : List MenuItem → Option (Control × Bool)
The first actionable item with ref r in a menu.
enabledOf (items : List MenuItem) (r : ControlRef) : Option Bool
Whether the item for r is enabled; none when the menu has no item for r.
checkedOf (items : List MenuItem) (r : ControlRef) : Option (Option Bool)
The item for r's checkmark (some none: not a checkbox); none when there is no item.
offset : Anchor → Nat
The anchor's distance in points.
Theorems 5
enabledRefsOf_sub (m : MenuItem) (r : ControlRef) : r ∈ m.enabledRefsOf → r ∈ m.refsOf
enabledRefs_sub (ms : List MenuItem) (r : ControlRef) : r ∈ enabledRefs ms → r ∈ refs ms
refs_append (xs ys : List MenuItem) : refs (xs ++ ys) = refs xs ++ refs ys
enabledRefs_append (xs ys : List MenuItem) : enabledRefs (xs ++ ys) = enabledRefs xs ++ enabledRefs ys
mem_refs_of_enabled {ms : List MenuItem} {r : ControlRef}
(h : r ∈ enabledRefs ms) : r ∈ refs msAn enabled item is an item.
Instances 10
instInhabitedStatusItem : Inhabited StatusItem
instReprStatusItem : Repr StatusItem
instInhabitedAnchor : Inhabited Anchor
instDecidableEqAnchor : DecidableEq Anchor
instReprAnchor : Repr Anchor
instDecidableEqScreenChoice : DecidableEq ScreenChoice
instInhabitedScreenChoice : Inhabited ScreenChoice
instReprScreenChoice : Repr ScreenChoice
instReprPanelView : Repr PanelView
instInhabitedPanelView : Inhabited PanelView