Cairn.Layout.Para
lean/Cairn/Layout/Para.lean
Wrapped text in layout
measure turns Node.para ts wr s into a clipping column (paraStyle wr) of one Sized.text
per line (paraLines). The lines come from Cairn.Text.Wrap.lines on the offsets of one
measurement of s, at wrapWidth wr aw. Because a para is a box of text once measured,
arrange, Laid, the frame and hit testing are unchanged, and every layout theorem
(Cairn.Layout.facts, Pressable, fitsIn_arrange) covers views with wrapped text in them.
What is proved here, for every metrics m and offered width aw:
para_lines_fit: every line's measured width is at most the wrap width (when that is non-negative), or the line is a single scalar;para_lines_tile: the lines, with break spaces only put back between and around them, are the text (withoutmaxLines);para_lines_tail/para_lines_head: withmaxLines, they are exactly the last / first lines of that;para_count: at mostmaxLineslines;para_height: ahugpara is lines × line height tall, each line one line height;layout_para_height: so is a root para's rect.
Imports Cairn.Layout.Rigid, Cairn.Text.WrapProofs
Definitions 2
paraOffsets (m : TextMetrics) (ts : TextStyle) (s : String) : Nat → Int
The offsets a para breaks with.
paraStrings (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) : List (List Char)
The lines' strings, as scalars.
Theorems 13
measure_para (m : TextMetrics) (aw : Int) (ts : TextStyle) (wr : Wrap) (s : String) : measure m aw (Node.para ts wr s) = Sized.box (paraStyle wr) none { w := resolve wr.width (contentSize Axis.column wr.lineSpacing (List.map Sized.size (paraLines m ts wr aw s))).w, h := resolve wr.height (contentSize Axis.column wr.lineSpacing (List.map Sized.size (paraLines m ts wr aw s))).h } (paraLines m ts wr aw s)
paraLines_eq (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) : paraLines m ts wr aw s = List.map (fun p => Sized.text ts (String.ofList (Text.Wrap.slice s.toList p)) { w := max 0 (Text.Wrap.width (paraOffsets m ts s) p), h := max 0 (m.lineHeight ts.font) }) (Text.Wrap.lines (paraOffsets m ts s) (wrapWidth wr aw) wr s.toList)
slice_length_le (cs : List Char) (p : Nat × Nat) : (Text.Wrap.slice cs p).length ≤ p.snd - p.fst
para_lines_fit (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) (hW : 0 ≤ wrapWidth wr aw) (k : Sized) : k ∈ paraLines m ts wr aw s → ∃ str sz, k = Sized.text ts str sz ∧ (sz.w ≤ wrapWidth wr aw ∨ str.length ≤ 1)
Lines fit. Every line of a para is at most the wrap width wide, or is one scalar.
paraStrings_eq (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) : paraStrings m ts wr aw s = List.map (Text.Wrap.slice s.toList) (Text.Wrap.lines (paraOffsets m ts s) (wrapWidth wr aw) wr s.toList)
para_lines_tile (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) (hm : wr.maxLines = none) : Text.Wrap.Tiles s.toList (paraStrings m ts wr aw s)
Lines tile the text. Without maxLines, the text is its lines with break spaces only
between and around them.
para_lines_tail (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) (n : Nat) (hm : wr.maxLines = some n) (hk : wr.keep = Keep.tail) : have all := List.map (Text.Wrap.slice s.toList) (Text.Wrap.allLines (paraOffsets m ts s) (wrapWidth wr aw) s.toList); ∃ pre, pre ++ paraStrings m ts wr aw s = all ∧ (paraStrings m ts wr aw s).length = min n all.length
Keep tail. With maxLines = some n and keep = .tail, the lines shown are exactly the
last min n k of the k lines the text breaks into.
para_lines_head (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) (n : Nat) (hm : wr.maxLines = some n) (hk : wr.keep = Keep.head) : have all := List.map (Text.Wrap.slice s.toList) (Text.Wrap.allLines (paraOffsets m ts s) (wrapWidth wr aw) s.toList); ∃ post, paraStrings m ts wr aw s ++ post = all ∧ (paraStrings m ts wr aw s).length = min n all.length
Keep head. With keep = .head, the first min n k lines.
para_count (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) (n : Nat) (hm : wr.maxLines = some n) : (paraLines m ts wr aw s).length ≤ n
Line count.
sum_replicate_heights (lh : Int) (ks : List Sized) : (∀ (k : Sized), k ∈ ks → k.size.h = lh) → (List.map (fun k => k.size.h) ks).sum = ↑ks.length * lh
para_line_height (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) (k : Sized) : k ∈ paraLines m ts wr aw s → k.size.h = max 0 (m.lineHeight ts.font)
Every line is one line height tall.
para_height (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) (hh : wr.height = Sizing.hug) : (measure m aw (Node.para ts wr s)).size.h = ↑(paraLines m ts wr aw s).length * max 0 (m.lineHeight ts.font) + gaps wr.lineSpacing (paraLines m ts wr aw s).length
Height. A hug para is exactly lines × line height tall, plus the line spacing between
lines.
layout_para_height (m : TextMetrics) (w : Size) (ts : TextStyle) (wr : Wrap) (s : String) (hh : wr.height = Sizing.hug) : (layout m w (Node.para ts wr s)).rect.h = ↑(paraLines m ts wr (windowRect w).w s).length * max 0 (m.lineHeight ts.font) + gaps wr.lineSpacing (paraLines m ts wr (windowRect w).w s).length
A para at the root of a view is lines × line height tall (plus line spacing), and wraps at the window's width unless its width is fixed.