Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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
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.
A minimalistic representation of text replacements.
A replacement
is given by a start location Replace
i n mi
, 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.
Instances
Amor p => Semigroup (Replace p) | The composition of two replacements The right-to-left order of composition has the nice property that when
Properties(x <> y) <> z === x <> (y <> z :: Replace (Plain Int)) |
(Show p, Show (Trans p)) => Show (Replace p) | |
Amor p => Shift (Replace p) | |
Defined in DiffLoc.Interval 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) # | |
(Eq p, Eq (Trans p)) => Eq (Replace p) | |
type Block (Replace p) | |
Defined in DiffLoc.Interval |
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)
.
Colline !l !c |
Instances
(Show l, Show c) => Show (Colline l c) | |
(Amor l, Origin c) => Amor (Colline l c) | |
(Origin l, Origin c) => Origin (Colline l c) | |
Defined in DiffLoc.Colline | |
(Eq l, Eq c) => Eq (Colline l c) | |
(Ord l, Ord c) => Ord (Colline l c) | |
Defined in DiffLoc.Colline | |
type Trans (Colline l c) | |
The space between two Colline
s.
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"
isVallee 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"
isVallee 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.
Vallee !dl !dc |
Instances
(Monoid l, Eq l, Monoid c) => Monoid (Vallee l c) | |
(Monoid l, Eq l, Semigroup c) => Semigroup (Vallee l c) | |
(Show dl, Show dc) => Show (Vallee dl dc) | |
(Eq dl, Eq dc) => Eq (Vallee dl dc) | |
(Ord dl, Ord dc) => Ord (Vallee dl dc) | |
Defined in DiffLoc.Colline |