Cairn.Text.Wrap
lean/Cairn/Text/Wrap.lean
Line breaking
Lean decides where wrapped text (Node.para) breaks; the host only measures. Everything here
works on the text as a list of Unicode scalars and on its caret offsets o : Nat → Int (o i
is the x offset before scalar i, from one Core Text shaping of the whole string, so a line
[a, b) is o b - o a wide). The rules (docs/layout.md, "Wrapped text"):
- Words are maximal runs of scalars other than the break space U+0020 (
isBreak). Lines break only between words, and the spaces at a break are dropped: a line runs from the start of its first word to the end of its last, with the spaces between its own words kept. - Greedy fill (
fill): a line takes words while the line, measured from its first scalar to the end of the next word, still fits; then the next word starts a new line. - Over-wide words. A word that starts a line and is wider than the width is cut into
pieces (
chunk): each the longest run of its scalars, from where the last one ended, that fits, and never less than one scalar. Every piece but the last is a line of its own; the last starts a line that later words may join. - At most
maxLines, keeping the first (Keep.head) or the last (Keep.tail) lines.
Theorems (Cairn.Text.WrapProofs): every line fits the width or is a single scalar; the lines
tile the text with only break spaces between and around them; the count is at most maxLines;
tail keeps exactly the last lines and head the first.
Each function is structural recursion (fuel where the measure isn't), so #guard and decide
evaluate it; the examples are in Cairn.Text.WrapProofs.
Imports Cairn.UI.Node
Definitions 17
isBreak (c : Char) : Bool
The break space: the only scalar a line breaks at, and the only one a break drops.
wordsFrom : List Char → Nat → Option Nat → List (Nat × Nat)
Maximal runs of non-break scalars, as [a, b) ranges. i is the index of the list's head
in the whole text; cur is where the run in progress started, if one is.
words (cs : List Char) : List (Nat × Nat)
The words of a text.
width (o : Nat → Int) (p : Nat × Nat) : Int
The width of the scalars [a, b).
cutGo (o : Nat → Int) (W : Int) (a b : Nat) : Nat → Nat → Nat
From a piece [a, c) that is allowed, add scalars while c < b and [a, c + 1) fits.
cut (o : Nat → Int) (W : Int) (a b : Nat) : Nat
Where the piece of [a, b) that starts at a ends: the longest prefix that fits, and at
least one scalar.
chunkGo (o : Nat → Int) (W : Int) (b : Nat) : Nat → Nat → List (Nat × Nat) × Nat × Nat
Cut the rest of a word, [a, b), into pieces: all but the last, and the last. fuel ≥ b - a
suffices.
chunk (o : Nat → Int) (W : Int) (p : Nat × Nat) : List (Nat × Nat) × Nat × Nat
A word as pieces (rule 3): itself if it fits, otherwise cut. The pieces but the last fill whole lines; the last one starts the line that continues with the next words.
fill (o : Nat → Int) (W : Int) : Nat × Nat → List (Nat × Nat) → List (Nat × Nat)
Greedy fill (rule 2): cur is the line so far. A word that doesn't fit on it starts a new
line, cut into pieces first if it is wider than a line.
breakAll (o : Nat → Int) (W : Int) : List (Nat × Nat) → List (Nat × Nat)
allLines (o : Nat → Int) (W : Int) (cs : List Char) : List (Nat × Nat)
Every line of cs at width W, as [a, b) scalar ranges, before maxLines.
keepLines {α : Type} : Option Nat → Keep → List α → List αAt most n lines, from the front or the back.
lines (o : Nat → Int) (W : Int) (wr : Wrap) (cs : List Char) : List (Nat × Nat)
The lines a wrapped text shows.
slice (cs : List Char) (p : Nat × Nat) : List Char
The scalars of the range [a, b).
mapSlices {β : Type} (f : Nat × Nat → List Char → β) (cs : List Char)
(ps : List (Nat × Nat)) : List βf applied to each range and its scalars: the specification. Each slice walks from the
start of the text, so this is quadratic in the text's length; the compiler runs
mapSlicesFast instead (mapSlices_eq).
mapSlicesGo {β : Type} (f : Nat × Nat → List Char → β) (cs : List Char) :
Nat → List Char → List (Nat × Nat) → List βcur is cs.drop base; ranges that start at or after base drop from there, so lines in
order cost one pass over the text. Any other range drops from the start.
mapSlicesFast {β : Type} (f : Nat × Nat → List Char → β) (cs : List Char)
(ps : List (Nat × Nat)) : List β
Theorems 2
mapSlicesGo_eq {β : Type} (f : Nat × Nat → List Char → β) (cs : List Char)
(ps : List (Nat × Nat)) (base : Nat) :
mapSlicesGo f cs base (List.drop base cs) ps = mapSlices f cs ps
mapSlices_eq : @mapSlices = @mapSlicesFast