Safe Haskell	Safe-Inferred
Language	Haskell2010

Cornelis.Diff

Description

Maintain a Diff between the text that Agda loaded most recently and the current Vim buffer. There is one such diff for every buffer, indexed by BufferNum.

This exports three functions: - resetDiff empties the diff when reloading Agda - recordUpdate adds a buffer update to the diff. - translateInterval applies the Diff to an interval coming from Agda, turning it into an interval for the current buffer.

Synopsis

resetDiff :: BufferNum -> Neovim CornelisEnv ()
translateInterval :: BufferNum -> Interval VimPos -> Neovim CornelisEnv (Maybe (Interval VimPos))
recordUpdate :: BufferNum -> Replace DPos -> Neovim CornelisEnv ()
data Replace p = Replace !p !(Trans p) !(Trans p)
data Colline l c = Colline !l !c
data Vallee dl dc = Vallee !dl !dc

Documentation

resetDiff :: BufferNum -> Neovim CornelisEnv () Source #

Reset the diff to an empty diff.

translateInterval :: BufferNum -> Interval VimPos -> Neovim CornelisEnv (Maybe (Interval VimPos)) Source #

Given an interval coming from Agda (a pair of start and end positions), find the corresponding interval in the current buffer. If an edit touches the interval, return Nothing.

recordUpdate :: BufferNum -> Replace DPos -> Neovim CornelisEnv () Source #

Add a buffer update (insertion or deletion) to the diff. The buffer update event coming from Vim is structured exactly how the diff-loc library expects it.

data Replace p #

A minimalistic representation of text replacements.

A replacement Replace i n m is given by a start location i, the length n of the interval to replace (source) and the length m of its replacement (target). This representation does not keep track of the actual data being inserted.

This may overapproximate the underlying text replacement, with intervals being wider than necessary. For example, the transformation from "abc" to "ac" could be represented by mkReplace 1 1 0 (replace "b" with "" at location 1), and also by mkReplace 0 2 1 (replace "ab" with "a" at location 0).

source   abc   abc
     -    b    ab
     +         a
target   a c   a c

Insertions are replacements with source intervals of length zero. Deletions are replacements with target intervals of length zero.

Constructors

Replace !p !(Trans p) !(Trans p)

Instances

Instances details

Amor p => Semigroup (Replace p)	The composition of two replacements `l <> r` represents the replacement `r` followed by `l`, as one replacement of an span that contains both `r` and `l`. The right-to-left order of composition has the nice property that when l `precedes r, `l <> r` can also be viewed intuitively as performing `l` and `r` simultaneously. Properties (x <> y) <> z === x <> (y <> z :: Replace (Plain Int))
Instance details Defined in DiffLoc.Interval Methods (<>) :: Replace p -> Replace p -> Replace p # sconcat :: NonEmpty (Replace p) -> Replace p # stimes :: Integral b => b -> Replace p -> Replace p #
(Show p, Show (Trans p)) => Show (Replace p)
Instance details Defined in DiffLoc.Interval Methods showsPrec :: Int -> Replace p -> ShowS # show :: Replace p -> String # showList :: [Replace p] -> ShowS #
Amor p => Shift (Replace p)
Instance details Defined in DiffLoc.Interval Associated Types type Block (Replace p) # Methods src :: Replace p -> Block (Replace p) # tgt :: Replace p -> Block (Replace p) # shiftBlock :: Replace p -> Block (Replace p) -> Maybe (Block (Replace p)) # coshiftBlock :: Replace p -> Block (Replace p) -> Maybe (Block (Replace p)) # shiftR :: Replace p -> Replace p -> Maybe (Replace p) # coshiftR :: Replace p -> Replace p -> Maybe (Replace p) # dual :: Replace p -> Replace p #
(Eq p, Eq (Trans p)) => Eq (Replace p)
Instance details Defined in DiffLoc.Interval Methods (==) :: Replace p -> Replace p -> Bool # (/=) :: Replace p -> Replace p -> Bool #
type Block (Replace p)
Instance details Defined in DiffLoc.Interval type Block (Replace p) = Interval p

data Colline l c #

Line and column coordinates.

The generalization over types of line and column numbers frees us from any specific indexing scheme, notably whether columns are zero- or one-indexed.

Example

abc
de
fgh

Assuming the lines and columns are both 1-indexed, "b" is at location (Colline 1 2) and "h" is at location (Colline 3 3).

Constructors

Colline !l !c

Instances

Instances details

(Show l, Show c) => Show (Colline l c)
Instance details Defined in DiffLoc.Colline Methods showsPrec :: Int -> Colline l c -> ShowS # show :: Colline l c -> String # showList :: [Colline l c] -> ShowS #
(Amor l, Origin c) => Amor (Colline l c)
Instance details Defined in DiffLoc.Colline Associated Types type Trans (Colline l c) # Methods (.+) :: Colline l c -> Trans (Colline l c) -> Colline l c # (.-.?) :: Colline l c -> Colline l c -> Maybe (Trans (Colline l c)) #
(Origin l, Origin c) => Origin (Colline l c)
Instance details Defined in DiffLoc.Colline Methods origin :: Colline l c #
(Eq l, Eq c) => Eq (Colline l c)
Instance details Defined in DiffLoc.Colline Methods (==) :: Colline l c -> Colline l c -> Bool # (/=) :: Colline l c -> Colline l c -> Bool #
(Ord l, Ord c) => Ord (Colline l c)
Instance details Defined in DiffLoc.Colline Methods compare :: Colline l c -> Colline l c -> Ordering # (<) :: Colline l c -> Colline l c -> Bool # (<=) :: Colline l c -> Colline l c -> Bool # (>) :: Colline l c -> Colline l c -> Bool # (>=) :: Colline l c -> Colline l c -> Bool # max :: Colline l c -> Colline l c -> Colline l c # min :: Colline l c -> Colline l c -> Colline l c #
type Trans (Colline l c)
Instance details Defined in DiffLoc.Colline type Trans (Colline l c) = Vallee (Trans l) (Trans c)

data Vallee dl dc #

The space between two Collines.

This type represents offsets between text locations x <= y as the number of newlines inbetween and the number of characters from the last new line to y, if there is at least one newline, or the number of characters from x to y.

Example

abc
de
fgh

The offset from "b" to "h" is Vallee 2 2 (two newlines to reach line 3, and from the beginning of that line, advance two characters to reach h).
The offset from "b" to "c" is Vallee 0 1 (advance one character).

The offset from "b" to "h" is actually the same as from "a" to "h" and from "c" to "h". Line-column offsets are thus not invertible. This was one of the main constraints in the design of the Amor class.

Constructors

Vallee !dl !dc

Instances

Instances details

(Monoid l, Eq l, Monoid c) => Monoid (Vallee l c)
Instance details Defined in DiffLoc.Colline Methods mempty :: Vallee l c # mappend :: Vallee l c -> Vallee l c -> Vallee l c # mconcat :: [Vallee l c] -> Vallee l c #
(Monoid l, Eq l, Semigroup c) => Semigroup (Vallee l c)
Instance details Defined in DiffLoc.Colline Methods (<>) :: Vallee l c -> Vallee l c -> Vallee l c # sconcat :: NonEmpty (Vallee l c) -> Vallee l c # stimes :: Integral b => b -> Vallee l c -> Vallee l c #
(Show dl, Show dc) => Show (Vallee dl dc)
Instance details Defined in DiffLoc.Colline Methods showsPrec :: Int -> Vallee dl dc -> ShowS # show :: Vallee dl dc -> String # showList :: [Vallee dl dc] -> ShowS #
(Eq dl, Eq dc) => Eq (Vallee dl dc)
Instance details Defined in DiffLoc.Colline Methods (==) :: Vallee dl dc -> Vallee dl dc -> Bool # (/=) :: Vallee dl dc -> Vallee dl dc -> Bool #
(Ord dl, Ord dc) => Ord (Vallee dl dc)
Instance details Defined in DiffLoc.Colline Methods compare :: Vallee dl dc -> Vallee dl dc -> Ordering # (<) :: Vallee dl dc -> Vallee dl dc -> Bool # (<=) :: Vallee dl dc -> Vallee dl dc -> Bool # (>) :: Vallee dl dc -> Vallee dl dc -> Bool # (>=) :: Vallee dl dc -> Vallee dl dc -> Bool # max :: Vallee dl dc -> Vallee dl dc -> Vallee dl dc # min :: Vallee dl dc -> Vallee dl dc -> Vallee dl dc #

Documentation

Instances

Properties

Example

Instances

Example

Instances