Cairn · module

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

Order

Structures 1

structure

Cairn.Mods

lean/Cairn/Input.lean:15
Mods : Type
Fields
shift : Bool
command : Bool
option : Bool
control : Bool
Instances

BEq Repr Inhabited

Inductive types 9

inductive

Cairn.Button

lean/Cairn/Input.lean:22
Button : Type
Constructors
primary : Button
secondary : Button
Instances

Repr BEq Inhabited

inductive

Cairn.Key

lean/Cairn/Input.lean:28
Key : Type

Keys the host reports by meaning. Printable text arrives as insertText, not as keys; char is only for shortcuts with a modifier.

Constructors
enter : Key
escape : Key
tab : Key
backspace : Key
delete : Key
left : Key
right : Key
up : Key
down : Key
home : Key
finish : Key
pageUp : Key
pageDown : Key
char (c : Char) : Key
menu : Key

The context-menu key: Shift-F10, or a PC keyboard's Menu key. It opens the focused control's menu (ControlMenu).

Instances

BEq Inhabited Repr

inductive

Cairn.Event

lean/Cairn/Input.lean:38
Event : Type

Host → Lean. Points are logical, in the window's content area.

Constructors
pointerMove (p : Point) : Event
pointerDown (p : Point) (button : Button) (clicks : Nat) (mods : Mods) : Event
pointerUp (p : Point) (button : Button) (mods : Mods) : Event
pointerExit : Event
scroll (p : Point) (dx dy : Int) : Event
key (k : Key) (mods : Mods) : 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
resize (size : Size) : 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).

reply (id : Nat) (r : Reply) : Event

The host's answer to request id.

subEvent (id : Nat) (e : SubEvent) : Event

An event from the subscription the runtime started as id.

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.

menuOpen (place : ClaimId) : Event

The status item place's menu is opening (menuWillOpen).

menuClose (place : ClaimId) : Event

The status item place's menu closed (menuDidClose); with the window's place, the control menu open in the window closed.

menuSelect (place : ClaimId) (ref : ControlRef) : Event

The person chose the item ref in the menu of surface place: a status item's menu, the app's items in the menu bar (Surface.menuBar), or, with the window's place, the control menu open in the window (UI.menu).

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").

Instances

Repr Inhabited BEq

inductive

Cairn.TextOp

lean/Cairn/Input.lean:108
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.

Constructors
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
Instances

Inhabited BEq Repr

inductive

Cairn.Action

lean/Cairn/Input.lean:125
Action : Type

Runtime → app. Every action names the control it came from, so every behaviour can be traced to a claim.

Constructors
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").

Instances

BEq Repr Inhabited

inductive

Cairn.Cursor

lean/Cairn/Input.lean:142
Cursor : Type
Constructors
arrow : Cursor
pointer : Cursor
text : Cursor
Instances

Inhabited Repr BEq

inductive

Cairn.ScrollTarget

lean/Cairn/Input.lean:147
ScrollTarget : Type

Where Effect.scrollTo moves a scroll box or a virtual list (docs/runtime.md, "Scrolling").

Constructors
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.

Instances

Inhabited Repr BEq

inductive

Cairn.Priority

lean/Cairn/Input.lean:159
Priority : Type

How urgently assistive apps should say an announcement (Effect.announce): low waits for what is being spoken; high interrupts it.

Constructors
low : Priority
high : Priority
Instances

BEq Repr Inhabited

inductive

Cairn.Effect

lean/Cairn/Input.lean:165
Effect : Type

App → host (and runtime).

Constructors
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.

announce (text : String) (priority : Priority) : Effect

Ask assistive apps (VoiceOver) to speak text, for news that has no focus of its own ("Couldn't like the post; it's back as it was"). Posted once, with exactly this text.

Instances

Repr BEq Inhabited

Definitions 5

def

Cairn.Event.isWorld

lean/Cairn/Input.lean:85
isWorld : Event → Bool

The events from the world (clock, reply, subEvent); every other event is input.

def

Cairn.Event.isMenu

lean/Cairn/Input.lean:91
isMenu : Event → Bool

The menu events (menuOpen, menuClose, menuSelect): about a status item's menu, not a laid tree.

def

Cairn.Event.isSurface

lean/Cairn/Input.lean:95
isSurface : Event → Bool
def

Cairn.Event.isLocal

lean/Cairn/Input.lean:101
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.

def

Cairn.Action.control

lean/Cairn/Input.lean:139
control : Action → ControlRef

Instances 36

instance

Cairn.instBEqMods

lean/Cairn/Input.lean:20
instBEqMods : BEq Mods
instance

Cairn.instReprMods

lean/Cairn/Input.lean:20
instReprMods : Repr Mods
instance

Cairn.instDecidableEqMods

lean/Cairn/Input.lean:20
instDecidableEqMods : DecidableEq Mods
instance

Cairn.instInhabitedMods

lean/Cairn/Input.lean:20
instInhabitedMods : Inhabited Mods
instance

Cairn.instReprButton

lean/Cairn/Input.lean:24
instReprButton : Repr Button
instance

Cairn.instDecidableEqButton

lean/Cairn/Input.lean:24
instDecidableEqButton : DecidableEq Button
instance

Cairn.instBEqButton

lean/Cairn/Input.lean:24
instBEqButton : BEq Button
instance

Cairn.instInhabitedButton

lean/Cairn/Input.lean:24
instInhabitedButton : Inhabited Button
instance

Cairn.instDecidableEqKey

lean/Cairn/Input.lean:35
instDecidableEqKey : DecidableEq Key
instance

Cairn.instBEqKey

lean/Cairn/Input.lean:35
instBEqKey : BEq Key
instance

Cairn.instInhabitedKey

lean/Cairn/Input.lean:35
instInhabitedKey : Inhabited Key
instance

Cairn.instReprKey

lean/Cairn/Input.lean:35
instReprKey : Repr Key
instance

Cairn.instReprEvent

lean/Cairn/Input.lean:82
instReprEvent : Repr Event
instance

Cairn.instInhabitedEvent

lean/Cairn/Input.lean:82
instInhabitedEvent : Inhabited Event
instance

Cairn.instBEqEvent

lean/Cairn/Input.lean:82
instBEqEvent : BEq Event
instance

Cairn.instInhabitedTextOp

lean/Cairn/Input.lean:120
instInhabitedTextOp : Inhabited TextOp
instance

Cairn.instBEqTextOp

lean/Cairn/Input.lean:120
instBEqTextOp : BEq TextOp
instance

Cairn.instReprTextOp

lean/Cairn/Input.lean:120
instReprTextOp : Repr TextOp
instance

Cairn.instBEqAction

lean/Cairn/Input.lean:136
instBEqAction : BEq Action
instance

Cairn.instReprAction

lean/Cairn/Input.lean:136
instReprAction : Repr Action
instance

Cairn.instInhabitedAction

lean/Cairn/Input.lean:136
instInhabitedAction : Inhabited Action
instance

Cairn.instInhabitedCursor

lean/Cairn/Input.lean:144
instInhabitedCursor : Inhabited Cursor
instance

Cairn.instReprCursor

lean/Cairn/Input.lean:144
instReprCursor : Repr Cursor
instance

Cairn.instDecidableEqCursor

lean/Cairn/Input.lean:144
instDecidableEqCursor : DecidableEq Cursor
instance

Cairn.instBEqCursor

lean/Cairn/Input.lean:144
instBEqCursor : BEq Cursor
instance

Cairn.instInhabitedScrollTarget

lean/Cairn/Input.lean:155
instInhabitedScrollTarget : Inhabited ScrollTarget
instance

Cairn.instDecidableEqScrollTarget

lean/Cairn/Input.lean:155
instDecidableEqScrollTarget : DecidableEq ScrollTarget
instance

Cairn.instReprScrollTarget

lean/Cairn/Input.lean:155
instReprScrollTarget : Repr ScrollTarget
instance

Cairn.instBEqScrollTarget

lean/Cairn/Input.lean:155
instBEqScrollTarget : BEq ScrollTarget
instance

Cairn.instBEqPriority

lean/Cairn/Input.lean:161
instBEqPriority : BEq Priority
instance

Cairn.instReprPriority

lean/Cairn/Input.lean:161
instReprPriority : Repr Priority
instance

Cairn.instDecidableEqPriority

lean/Cairn/Input.lean:161
instDecidableEqPriority : DecidableEq Priority
instance

Cairn.instInhabitedPriority

lean/Cairn/Input.lean:161
instInhabitedPriority : Inhabited Priority
instance

Cairn.instReprEffect

lean/Cairn/Input.lean:200
instReprEffect : Repr Effect
instance

Cairn.instBEqEffect

lean/Cairn/Input.lean:200
instBEqEffect : BEq Effect
instance

Cairn.instInhabitedEffect

lean/Cairn/Input.lean:200
instInhabitedEffect : Inhabited Effect