package mosaic
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=9e4e90d17f9b2af1b07071fe425bc2c519c849c4f1d1ab73cde512be2d874849
sha512=06e9c4a741590942e81a27738d0b5c0413fafec8cf3b7dae047ad69f155e7b718aa4223818dc161b7d028efffcfd3365905e264d6fd31d453910ddfa91dcf9b9
doc/mosaic.ui/Mosaic_ui/Selection/index.html
Module Mosaic_ui.SelectionSource
Text selections with anchor and focus points.
Text selections with anchor and focus points.
A selection spans from an anchor to a focus point in 0-based terminal coordinates. The anchor is the fixed starting point of the selection gesture; the focus is the current endpoint. Selections support dynamic anchor positioning via a callback, useful for scrollable content where the anchor moves as the viewport scrolls.
See also t for the mutable selection type and create for construction.
Points and bounds
The type for 2D coordinates in 0-based column and row indices.
pp_point ppf p formats p on ppf as (x, y).
equal_point a b is true iff a and b have the same coordinates.
The type for bounding rectangles in cell coordinates.
The rectangle covers all cells satisfying x <= col < x + width and y <= row < y + height. Both the anchor and focus cells are included in the selection, so a single-cell selection has width = 1 and height = 1.
pp_bounds ppf b formats b on ppf as {x=...; y=...; w=...; h=...}.
equal_bounds a b is true iff a and b describe the same rectangle.
The type for selection endpoints in local coordinates, after transformation via to_local.
pp_local_bounds ppf lb formats lb on ppf as {anchor=...; focus=...}.
equal_local_bounds a b is true iff both endpoints match.
Selections
The type for mutable text selections.
pp ppf t formats a human-readable representation of t on ppf.
create ?anchor_position ~anchor ~focus () is a new active selection from anchor to focus.
The selection is created with is_active, is_dragging, and is_start all true.
anchor_position defaults to a static function returning anchor. When provided, the anchor is recomputed by calling it on each access to anchor, which is useful for selections in scrollable content.
See also set_anchor and set_focus.
Position
anchor t is the anchor point of t, i.e. where the selection gesture started. If an anchor_position callback was provided at create, it is called on each access to obtain the current position.
focus t is the focus point of t, i.e. the current endpoint of the selection.
set_anchor t p sets the anchor of t to p. Any anchor_position callback provided at create is replaced by a static value.
bounds t is the bounding rectangle enclosing t.
Both the anchor and focus cells are included. A selection from (x0, y0) to (x1, y1) produces width = |x1 - x0| + 1 and height = |y1 - y0| + 1.
See also bounds.
State
is_dragging t is true iff the user is actively dragging to extend t.
is_start t is true iff t is on the first frame of a new selection. Consumers use this to distinguish starting a new selection from extending an existing one.
Converting
to_local t ~origin is t's anchor and focus in coordinates relative to origin.
See also local_bounds.