package grenier

Type of semi-persistent buffers

Create a new lineage of buffers

Clear contents of a buffer

true iff is buffer empty ?

Shift contents of the buffer by removing len units starting at at. Valid iff at >= 0 && len >= 0. Cursors exactly at position at are removed iff called with ~left_of:().

Shift contents of the buffer by inserting len units starting at at. Valid iff at >= 0 && len >= 0. Cursors exactly at position at are shifted iff called with ~left_of:().

Type of cursors

Is a cursor member of a buffer ?

Find value associated to a cursor, or raise Not_found

Compare the position of two cursors

Get the physical position of a cursor in a revision of a buffer

Create a new cursors at position at Valid iff at >= 0.

Insert or update a cursor. Cursor is inserted at the left-most valid position.

Insert or update a cursor. Cursor is inserted at the right-most valid position before buffer end.

rem_cursor t c removes a cursor from the buffer. Valid iff member t c.

cursor_after c creates a cursor that is immediately after c.

cursor_before c creates a cursor that is immediately before c.

cursor_at_origin t creates a cursor that is minimal for t (before all other cursors in t)

Remove anything between two cursors. remove_between t a b is valid iff member t a && member t b && compare a b <= 0

remove_before t c len removes len units before c. Valid iff member t c && len >= 0.

remove_after t c len removes len units after c. Valid iff member t c && len >= 0.

insert_before t c len inserts len units before c. Valid iff member t c && len >= 0.

insert_before t c len inserts len units after c. Valid iff member t c && len >= 0.

find_before t at finds the last cursor c in t satisfying position t c <= at

find_after t at finds the first cursor c in t satisfying position t c >= at

seek_before t c finds the last cursor c' in t satisfying compare c' c < 0

seek_after t c finds the first cursor c' in t satisfying compare c' c > 0