Cairn.Text.Field
lean/Cairn/Text/Field.lean
Single-line text editing
Field is the editing model behind every text field: the text, caret, anchor, IME marked range,
undo and redo stacks, and placeholder. Field.apply gives the meaning of every TextOp;
Field.view turns a field into the FieldView the view layer draws.
The text is a List Char, so every index is a Unicode scalar position, the same unit as
String.length and TextMetrics.offsets. Lists are used rather than String because every
edit is a splice (take a ++ s ++ drop b), and core Lean's List lemmas about take, drop
and length make the proofs short; String's byte-indexed API would put a UTF-8 decoding step
between every theorem and its statement. The view converts with String.ofList
(String.length_ofList keeps the indices meaning the same thing).
The behaviour is specified, op by op and against macOS's NSTextView, in docs/text.md.
Theorems are in Cairn.Text.Proofs.
Imports Cairn.Input, Cairn.UI.Node
Structures 4
Snapshot : Type
What an undo step restores: the text and the selection.
text : List Charcaret : Natanchor : NatField : Type
text : List CharUnicode scalars; never contains a line break (SingleLine).
caret : NatWhere the insertion point is, and the end of the selection that moves.
anchor : NatThe fixed end of the selection. The selection is [min caret anchor, max caret anchor).
marked : Option (Nat × Nat)
IME composition in progress, [start, end) of text.
undoStack : List Snapshot
Most recent first. Each entry is the state before an undoable edit.
redoStack : List Snapshot
Most recent first. Cleared by every edit that changes the text.
typing : BoolThe last op was a typing insert; another one at a collapsed caret joins its undo step.
placeholder : StringWF (f : Field) : Prop
Every index is a position in the text, and the text is a single line.
caret_le : f.caret ≤ f.text.length
anchor_le : f.anchor ≤ f.text.length
marked_le : a ≤ b ∧ b ≤ f.text.length
single : SingleLine f.text
undo_wf : s.WF
redo_wf : s.WF
SecureField : Type
A password field: a Field whose history is always empty.
field : Field
Definitions 45
isLineBreak (c : Char) : Bool
Scalars that would start a new line. A single-line field never contains them: inserted and
pasted text has each one replaced by a space, as NSTextField does in single-line mode.
SingleLine (t : List Char) : PropThe text a field may contain: no line breaks.
flatten (c : Char) : Char
One scalar as a single-line field stores it: a line break becomes a space.
clean (s : String) : List Char
s as scalars, each line break replaced by a space. Same length as s.
isWordChar (c : Char) : Bool
A word is a maximal run of word characters: ASCII letters, digits and _, and every non-ASCII
scalar except the Unicode spaces below. Everything else (ASCII punctuation and spaces) separates
words. This is deliberately simpler than NSTextView, which uses ICU word boundaries and a
dictionary for scripts without spaces; see docs/text.md.
span (p : Char → Bool) : List Char → Nat
The length of the longest prefix of l whose scalars satisfy p.
wordLeft (t : List Char) (i : Nat) : Nat
Where Option-Left goes from i: back over separators, then back over a word.
wordRight (t : List Char) (i : Nat) : Nat
Where Option-Right goes from i: forward over separators, then forward over a word.
splice (t : List Char) (a b : Nat) (s : List Char) : List Char
t with [a, b) replaced by s.
empty (placeholder : String := "") : Field
An empty field.
ofString (s : String) (placeholder : String := "") : Field
A field holding s (line breaks removed) with the caret at the end.
lo (f : Field) : Nat
hi (f : Field) : Nat
len (f : Field) : Nat
selected (f : Field) : List Char
The selected scalars, [lo, hi).
snapshot (f : Field) : Snapshot
textString (f : Field) : String
target (f : Field) : Nat × Nat
The range an insertion or composition replaces: the marked text if there is any, else the selection.
targetOr (f : Field) : Option (Nat × Nat) → Nat × Nat
The range an input-method edit replaces: the explicit replace range when the input system
gives one (press-and-hold accents, reconversion, Korean IMEs that rewrite the last syllable),
clamped into the text, else target.
edit (f : Field) (text : List Char) (caret anchor : Nat) (push typing : Bool) : Field
Set the text and selection after an edit. When the text really changes, the old state is
pushed for undo (if push) and redo is cleared; when it doesn't, only the selection moves and
nothing is recorded.
moveTo (f : Field) (i : Nat) (extend : Bool) : Field
Move the caret to i, keeping the anchor when extending. Ends any composition.
deleteRange (f : Field) (a b : Nat) (coalesce : Bool := false) : Field
Delete [a, b). With coalesce, the deletion joins an open typing step and keeps it open
(Backspace while typing); otherwise it is its own undo step.
deleteSelOr (f : Field) (a b : Nat) (coalesce : Bool := false) : Field
Delete the selection if there is one (its own undo step), else [a, b).
insert (f : Field) (s : String) (replace : Option (Nat × Nat) := none) : Field
paste (f : Field) (s : String) : Field
Like insert, but always its own undo step (unless it commits a composition).
setMarked (f : Field) (s : String) (selStart selLen : Nat) (replace : Option (Nat × Nat) := none) : Field
IME composition: replace the marked text (or, when composition starts, the selection) with
s, mark it, and put the selection at [selStart, selStart + selLen) within it, clamped.
Starting a composition opens an undo step; the whole composition, through its commit, is that
one step. An empty composition ends it. replace is as for insert.
unmark (f : Field) : Field
Commit the composition as it stands; the text and selection stay.
undo (f : Field) : Field × List Effect
redo (f : Field) : Field × List Effect
clipboard (f : Field) : List Effect
apply : TextOp → Field → Field × List Effect
The meaning of every TextOp. See docs/text.md.
applyAll (f : Field) (ops : List TextOp) : Field
Apply ops in order, dropping effects.
iterate (op : TextOp) : Nat → Field → Field
Apply op n times.
view (f : Field) (focused : Bool) : FieldView
What the view layer draws.
WF (s : Snapshot) : Prop
bullet : CharWhat a secure field draws for each scalar.
bullets (n : Nat) : String
n bullets.
empty (placeholder : String := "") : SecureField
An empty secure field.
text (f : SecureField) : String
What was typed. Only for the one request that sends it (with redact := true).
len (f : SecureField) : Nat
forget (f : Field) : Field
The field without undo or redo history.
apply : TextOp → SecureField → SecureField × List Effect
Like Field.apply, except that copy, cut, undo and redo beep and change nothing, and no
history is kept.
applyAll (f : SecureField) (ops : List TextOp) : SecureField
Apply ops in order, dropping effects.
view (f : SecureField) (focused : Bool) : FieldView
What the view layer draws: a bullet per scalar, the field's selection and composition, and
secure.
Agree (f g : SecureField) : Prop
Two secure fields that show the same: the same number of scalars, selection, composition and placeholder, whatever the scalars are.
Theorems 2
view_text (f : SecureField) (b : Bool) : (f.view b).text.toList = List.replicate f.field.text.length bullet ∧ (f.view b).secure = true
Bullets: the view's text is one bullet per scalar typed.
view_agree {f g : SecureField} (h : f.Agree g) (b : Bool) :
f.view b = g.view bThe view hides the text: two secure fields that agree on everything but which scalars were typed have the same view, so nothing built from it (layout, the frame, the accessibility mirror, a dump) can tell them apart.
Instances 12
instReprSnapshot : Repr Snapshot
instBEqSnapshot : BEq Snapshot
instInhabitedSnapshot : Inhabited Snapshot
instDecidableEqSnapshot : DecidableEq Snapshot
instDecidableEqField : DecidableEq Field
instReprField : Repr Field
instInhabitedField : Inhabited Field
instBEqField : BEq Field
instDecidableEqSecureField : DecidableEq SecureField
instBEqSecureField : BEq SecureField
instReprSecureField : Repr SecureField
instInhabitedSecureField : Inhabited SecureField
Characters
State
Primitive transitions
Ops
Well-formedness
Secure fields
A secure field is a password field, as NSSecureTextField: the same editing model, but it
draws a bullet per scalar, refuses copy and cut with a beep, and keeps no undo history. It wraps
a Field rather than flagging one, so Field.apply and every theorem and claim stated with it
mean what they did. The typed text is in Lean (typed text always is) but never in its view:
view puts bullets in FieldView.text, so what layout measures, the frame draws and every dump
prints is its length only (SecureField.view_agree, Dump.secure_frame). Theorems are in
Cairn.Text.Proofs; the rules are in docs/text.md, "Secure fields".