Cairn.Input
lean/Cairn/Input.lean
What the host sends Lean (Event), what the runtime gives an app (Action), and what an
app asks the host to do (Effect).
Imports Cairn.Geometry, Cairn.Claim, Cairn.Effects
Structures 1
Mods : Type
shift : Boolcommand : Booloption : Boolcontrol : BoolInductive types 9
Button : Type
Key : Type
Keys the host reports by meaning. Printable text arrives as insertText, not as keys;
char is only for shortcuts with a modifier.
Event : Type
Host → Lean. Points are logical, in the window's content area.
pointerExit : Event
insertText (s : String) (replace : Option (Nat × Nat) := none) : Event
Committed text from the input system (typing, IME commit, dictation). With replace,
the text replaces that range [a, b) of the focused field (scalar indices) instead of the
selection.
setMarked (s : String) (selStart selLen : Nat) (replace : Option (Nat × Nat) := none) : Event
IME composition: the marked text and the selection within it, optionally replacing the
range replace of the focused field.
unmark : Event
copy : Event
cut : Event
selectAll : Event
undo : Event
redo : Event
paste (s : String) : Event
scale (percent : Nat) : Event
Backing scale × 100 (200 on a Retina display).
windowFocus (focused : Bool) : Event
clock (t : Time) : Event
The host's time. The host sends one first in every batch, and before any later event that arrived a millisecond or more later (docs/effects.md).
surface (place : ClaimId) (e : Event) : Event
A surface-local event (pointer, key, text, resize, scale, focus) for the surface whose
place claim is place (docs/surfaces.md). A bare local event is the window's, as in M1.
frame : Event
The runtime's own, never the host's (it has no encoding): the end of a batch, before the
frame is drawn. Runtime.steps runs it after every batch; it compares what is on screen with
the last frame and delivers Action.appear (docs/runtime.md, "Appear").
TextOp : Type
Edits to a text field's model. The runtime turns key and text events into these; the
semantics are Cairn.Text.Field.apply.
insert (s : String) : TextOp
deleteBackward : TextOp
deleteForward : TextOp
deleteWordBackward : TextOp
deleteWordForward : TextOp
moveLeft (extend : Bool) : TextOp
moveRight (extend : Bool) : TextOp
moveWordLeft (extend : Bool) : TextOp
moveWordRight (extend : Bool) : TextOp
moveHome (extend : Bool) : TextOp
moveEnd (extend : Bool) : TextOp
setCaret (i : Nat) (extend : Bool) : TextOp
selectAll : TextOp
setMarked (s : String) (selStart selLen : Nat) : TextOp
unmark : TextOp
cut : TextOp
copy : TextOp
paste (s : String) : TextOp
undo : TextOp
redo : TextOp
Action : Type
Runtime → app. Every action names the control it came from, so every behaviour can be traced to a claim.
press (c : ControlRef) : Action
doublePress (c : ControlRef) : Action
edit (c : ControlRef) (op : TextOp) : Action
submit (c : ControlRef) : Action
cancel (c : ControlRef) : Action
blur (c : ControlRef) : Action
appear (c : ControlRef) : Action
The control c, marked Control.appear, came on screen: at the end of a batch it has a
visible part, and at the end of the last batch it had none or wasn't there. The runtime's, not
a person's: no pointer or key makes it directly (docs/runtime.md, "Appear").
Cursor : Type
ScrollTarget : Type
Where Effect.scrollTo moves a scroll box or a virtual list (docs/runtime.md, "Scrolling").
start : ScrollTarget
Offset 0: the content's start.
finish : ScrollTarget
The furthest the offset goes: the content's end at the box's end.
key (k : Nat) : ScrollTarget
A virtual list's row with key k at the top of the box. Nothing on a plain scroll box, or
for a key the list doesn't have.
Priority : Type
How urgently assistive apps should say an announcement (Effect.announce): low waits for
what is being spoken; high interrupts it.
Effect : Type
App → host (and runtime).
setClipboard (s : String) : Effect
beep : Effect
focus (c : ControlRef) : Effect
Move keyboard focus to the control c. The runtime runs this one, not the host: after the
step's actions it sets ui.focus := some c, and keeps it only if c is a focusable control
of the new tree (docs/runtime.md). No blur is delivered for a field it takes focus from.
The host decodes it and does nothing.
setTimer (name : String) (ms : Nat) : Effect
Start (or restart) the timer name, due ms milliseconds from now. The runtime keeps
timers; the host only wakes it (docs/effects.md).
cancelTimer (name : String) : Effect
Forget the timer name; nothing if it isn't set.
request (id : Nat) (r : Request) : Effect
Ask the host to do r; it answers with Msg.reply id _, exactly once. At most
App.maxInFlight requests of capped kinds (Request.Kind.capped) are with the host at a time;
the runtime holds the rest and sends them, oldest first, as slots free.
cancelRequest (id : Nat) : Effect
Withdraw request id (docs/effects.md, "Requests in flight"). Its reply never reaches the
app. A request still waiting for a slot is dropped and never sent; one already sent is cancelled
on the host (URLSessionTask.cancel), and its id stays taken until the host's one reply to it
arrives, which the runtime swallows. Nothing if id is not pending.
quit : Effect
End the app. The host terminates after running the frame's other effects.
scrollTo (box : ControlRef) (to : ScrollTarget) : Effect
Move the scroll box or virtual list box (its Style.scrollRef) to to, clamped as every
offset is. The runtime runs this one, like focus: after the step's deliveries and layout it
sets the offset against the tree just laid and lays out again (docs/runtime.md, "Scrolling").
A box not on screen is left alone. The host decodes it and does nothing.
badge (label : Option String) : Effect
Set the Dock tile's badge to label; none clears it (docs/effects.md, "The Dock badge
and announcements"). The host shows exactly the label; Lean decides what it says.
Definitions 5
isWorld : Event → Bool
isMenu : Event → Bool
The menu events (menuOpen, menuClose, menuSelect): about a status item's menu, not a
laid tree.
isSurface : Event → Bool
isLocal : Event → Bool
Surface-local events: input a Metal surface receives (pointer, keys, text, editing, size,
scale, focus). Only these may be addressed to a surface with Event.surface.
control : Action → ControlRef
Instances 36
instBEqMods : BEq Mods
instReprMods : Repr Mods
instDecidableEqMods : DecidableEq Mods
instInhabitedMods : Inhabited Mods
instReprButton : Repr Button
instDecidableEqButton : DecidableEq Button
instBEqButton : BEq Button
instInhabitedButton : Inhabited Button
instDecidableEqKey : DecidableEq Key
instBEqKey : BEq Key
instInhabitedKey : Inhabited Key
instReprKey : Repr Key
instReprEvent : Repr Event
instInhabitedEvent : Inhabited Event
instBEqEvent : BEq Event
instInhabitedTextOp : Inhabited TextOp
instBEqTextOp : BEq TextOp
instReprTextOp : Repr TextOp
instBEqAction : BEq Action
instReprAction : Repr Action
instInhabitedAction : Inhabited Action
instInhabitedCursor : Inhabited Cursor
instReprCursor : Repr Cursor
instDecidableEqCursor : DecidableEq Cursor
instBEqCursor : BEq Cursor
instInhabitedScrollTarget : Inhabited ScrollTarget
instDecidableEqScrollTarget : DecidableEq ScrollTarget
instReprScrollTarget : Repr ScrollTarget
instBEqScrollTarget : BEq ScrollTarget
instBEqPriority : BEq Priority
instReprPriority : Repr Priority
instDecidableEqPriority : DecidableEq Priority
instInhabitedPriority : Inhabited Priority
instReprEffect : Repr Effect
instBEqEffect : BEq Effect
instInhabitedEffect : Inhabited Effect