Cairn · module

Cairn.Layout.Scroll

lean/Cairn/Layout/Scroll.lean

Scroll boxes: what holds of every one

The framework's facts about scroll boxes (Style.scroll, docs/layout.md, "Scroll boxes"), for any scroll box, any children, any text metrics and any window:

  • scroll_rects, scroll_column_rects: the children are where the same box without scrolling puts them, moved back by the offset (in a column: same x, width and height, y less the offset).
  • layout_scrollApart: in a row or column scroll box, the children's rects don't overlap, and what shows of anything under the box is inside the box.
  • pressed_where_visible: in a Pressable view, a control with a visible part is hit at that part's centre, and a control with none is hit nowhere.

The test fixture states them for its own scroll box as claims (fixture^11–^13, test/fixture/lean/Checks/Scroll.lean).

Imports Cairn.Layout.Proofs, Cairn.Layout.Bridge

Order

Definitions 1

def

Cairn.Layout.ScrollApart

lean/Cairn/Layout/Scroll.lean:49
ScrollApart : Laid → Prop

At a row or column scroll box: its children's rects are pairwise disjoint, and every node under it shows only inside it (each nonempty visible part, rect ∩ clip, is inside the box).

Theorems 4

theorem

Cairn.Layout.scroll_rects

provedlean/Cairn/Layout/Scroll.lean:26
scroll_rects (m : TextMetrics) (c r : Rect) (aw : Int) (st : Style)
  (ctl : Option Control) (kids : List Node) (o : Int) :
  List.map Laid.rect
      (arrange m c r
          (measure m aw
            (Node.box
              { axis := st.axis, width := st.width, height := st.height,
                padding := st.padding, gap := st.gap, align := st.align,
                justify := st.justify, background := st.background, border := st.border,
                radius := st.radius, clip := st.clip, corner := st.corner,
                shadow := st.shadow, paint := st.paint, image := st.image, scroll := some o,
                scrollRef := st.scrollRef, rows := st.rows, menu := st.menu }
              ctl kids))).children =
    List.map (Rect.scrollBy (Axis.horiz st.axis) o)
      (List.map Laid.rect
        (arrange m c r
            (measure m aw
              (Node.box
                { axis := st.axis, width := st.width, height := st.height,
                  padding := st.padding, gap := st.gap, align := st.align,
                  justify := st.justify, background := st.background, border := st.border,
                  radius := st.radius, clip := st.clip, corner := st.corner,
                  shadow := st.shadow, paint := st.paint, image := st.image,
                  scrollRef := st.scrollRef, rows := st.rows, menu := st.menu }
                ctl kids))).children)

Children at the unscrolled place, moved back. Laid out anywhere, a scroll box with offset o puts each child at the rect the same box without scroll gives it, moved back by o along its axis (Rect.scrollBy: left in a row, up otherwise).

theorem

Cairn.Layout.scroll_column_rects

provedlean/Cairn/Layout/Scroll.lean:37
scroll_column_rects (m : TextMetrics) (c r : Rect) (aw : Int) (st : Style)
  (ctl : Option Control) (kids : List Node) (o : Int) (hcol : st.axis = Axis.column) :
  List.map Laid.rect
      (arrange m c r
          (measure m aw
            (Node.box
              { axis := st.axis, width := st.width, height := st.height,
                padding := st.padding, gap := st.gap, align := st.align,
                justify := st.justify, background := st.background, border := st.border,
                radius := st.radius, clip := st.clip, corner := st.corner,
                shadow := st.shadow, paint := st.paint, image := st.image, scroll := some o,
                scrollRef := st.scrollRef, rows := st.rows, menu := st.menu }
              ctl kids))).children =
    List.map (fun q => { x := q.x, y := q.y - o, w := q.w, h := q.h })
      (List.map Laid.rect
        (arrange m c r
            (measure m aw
              (Node.box
                { axis := st.axis, width := st.width, height := st.height,
                  padding := st.padding, gap := st.gap, align := st.align,
                  justify := st.justify, background := st.background, border := st.border,
                  radius := st.radius, clip := st.clip, corner := st.corner,
                  shadow := st.shadow, paint := st.paint, image := st.image,
                  scrollRef := st.scrollRef, rows := st.rows, menu := st.menu }
                ctl kids))).children)

In a column, y less the offset. A column scroll box with offset o puts each child where the same column without scrolling does, o points higher: same x, width and height.

theorem

Cairn.Layout.layout_scrollApart

provedlean/Cairn/Layout/Scroll.lean:57
layout_scrollApart (m : TextMetrics) (w : Size) (n : Node) :
  Laid.Everywhere ScrollApart (layout m w n)

Apart, and inside the box. Every row or column scroll box in every laid-out view keeps its children apart and shows them only inside itself.

theorem

Cairn.Layout.pressed_where_visible

provedlean/Cairn/Layout/Scroll.lean:70
pressed_where_visible {m : TextMetrics} {w : Size} {n : Node}
  (hp : Pressable w (layout m w n)) {t : Runtime.Target}
  (ht : t ∈ Runtime.targets (layout m w n)) :
  (t.visible.nonempty → Runtime.hitTest (layout m w n) t.visible.center = some t.control) ∧
    (¬t.visible.nonempty → ∀ (p : Point), Runtime.hitTarget (layout m w n) p ≠ some t)

Pressed where it shows, and nowhere else. In a Pressable view, a control with a nonempty visible part is hit at that part's centre, and a control scrolled wholly out of view (an empty visible part) is the hit at no point.