{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
module Cornelis.Vim where
import Control.Lens ((%~), _head, _last, (&))
import Cornelis.Offsets
import Cornelis.Types
import Cornelis.Utils (objectToInt, savingCurrentPosition, savingCurrentWindow)
import Data.Foldable (toList)
import Data.Int
import qualified Data.Map as M
import qualified Data.Text as T
import Data.Text.Encoding (encodeUtf8)
import qualified Data.Vector as V
import Neovim
import Neovim.API.Text
vimFirstLine :: Int64
vimFirstLine :: Int64
vimFirstLine = Int64
0
vimLastLine :: Int64
vimLastLine :: Int64
vimLastLine = -Int64
1
getWindowCursor :: Window -> Neovim env AgdaPos
getWindowCursor :: forall env. Window -> Neovim env AgdaPos
getWindowCursor Window
w = do
(Int64 -> Index 'Line 'OneIndexed
forall a (e :: Unit). Integral a => a -> Index e 'OneIndexed
toOneIndexed -> Index 'Line 'OneIndexed
row, Int64 -> Index 'Byte 'ZeroIndexed
forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed -> Index 'Byte 'ZeroIndexed
col) <- Window -> Neovim env (Int64, Int64)
forall env. Window -> Neovim env (Int64, Int64)
window_get_cursor Window
w
let line :: Index 'Line 'ZeroIndexed
line = Index 'Line 'OneIndexed -> Index 'Line 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex Index 'Line 'OneIndexed
row
Buffer
b <- Window -> Neovim env Buffer
forall env. Window -> Neovim env Buffer
window_get_buffer Window
w
Buffer -> VimPos -> Neovim env AgdaPos
forall env. Buffer -> VimPos -> Neovim env AgdaPos
unvimify Buffer
b (Index 'Line 'ZeroIndexed -> Index 'Byte 'ZeroIndexed -> VimPos
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos Index 'Line 'ZeroIndexed
line Index 'Byte 'ZeroIndexed
col)
getpos :: Buffer -> Char -> Neovim env AgdaPos
getpos :: forall env. Buffer -> Char -> Neovim env AgdaPos
getpos Buffer
b Char
mark = do
ObjectArray [Object
_, forall a. Num a => Object -> Maybe a
objectToInt @Int -> Just (Int -> Index 'Line 'OneIndexed
forall a (e :: Unit). Integral a => a -> Index e 'OneIndexed
toOneIndexed -> Index 'Line 'OneIndexed
line), forall a. Num a => Object -> Maybe a
objectToInt @Int -> Just (Int -> Index 'Byte 'OneIndexed
forall a (e :: Unit). Integral a => a -> Index e 'OneIndexed
toOneIndexed -> Index 'Byte 'OneIndexed
col), Object
_]
<- Text -> Vector Object -> Neovim env Object
forall env. Text -> Vector Object -> Neovim env Object
vim_call_function Text
"getpos" (Vector Object -> Neovim env Object)
-> Vector Object -> Neovim env Object
forall a b. (a -> b) -> a -> b
$ [Object] -> Vector Object
forall a. [a] -> Vector a
V.fromList [ByteString -> Object
ObjectString (ByteString -> Object) -> ByteString -> Object
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
encodeUtf8 (Text -> ByteString) -> Text -> ByteString
forall a b. (a -> b) -> a -> b
$ Char -> Text
T.singleton Char
mark]
Buffer -> VimPos -> Neovim env AgdaPos
forall env. Buffer -> VimPos -> Neovim env AgdaPos
unvimify Buffer
b (Index 'Line 'ZeroIndexed -> Index 'Byte 'ZeroIndexed -> VimPos
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos (Index 'Line 'OneIndexed -> Index 'Line 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex Index 'Line 'OneIndexed
line) (Index 'Byte 'OneIndexed -> Index 'Byte 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex Index 'Byte 'OneIndexed
col))
data SearchMode = Forward | Backward
deriving (SearchMode -> SearchMode -> Bool
(SearchMode -> SearchMode -> Bool)
-> (SearchMode -> SearchMode -> Bool) -> Eq SearchMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SearchMode -> SearchMode -> Bool
== :: SearchMode -> SearchMode -> Bool
$c/= :: SearchMode -> SearchMode -> Bool
/= :: SearchMode -> SearchMode -> Bool
Eq, Eq SearchMode
Eq SearchMode =>
(SearchMode -> SearchMode -> Ordering)
-> (SearchMode -> SearchMode -> Bool)
-> (SearchMode -> SearchMode -> Bool)
-> (SearchMode -> SearchMode -> Bool)
-> (SearchMode -> SearchMode -> Bool)
-> (SearchMode -> SearchMode -> SearchMode)
-> (SearchMode -> SearchMode -> SearchMode)
-> Ord SearchMode
SearchMode -> SearchMode -> Bool
SearchMode -> SearchMode -> Ordering
SearchMode -> SearchMode -> SearchMode
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SearchMode -> SearchMode -> Ordering
compare :: SearchMode -> SearchMode -> Ordering
$c< :: SearchMode -> SearchMode -> Bool
< :: SearchMode -> SearchMode -> Bool
$c<= :: SearchMode -> SearchMode -> Bool
<= :: SearchMode -> SearchMode -> Bool
$c> :: SearchMode -> SearchMode -> Bool
> :: SearchMode -> SearchMode -> Bool
$c>= :: SearchMode -> SearchMode -> Bool
>= :: SearchMode -> SearchMode -> Bool
$cmax :: SearchMode -> SearchMode -> SearchMode
max :: SearchMode -> SearchMode -> SearchMode
$cmin :: SearchMode -> SearchMode -> SearchMode
min :: SearchMode -> SearchMode -> SearchMode
Ord, Int -> SearchMode -> ShowS
[SearchMode] -> ShowS
SearchMode -> String
(Int -> SearchMode -> ShowS)
-> (SearchMode -> String)
-> ([SearchMode] -> ShowS)
-> Show SearchMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SearchMode -> ShowS
showsPrec :: Int -> SearchMode -> ShowS
$cshow :: SearchMode -> String
show :: SearchMode -> String
$cshowList :: [SearchMode] -> ShowS
showList :: [SearchMode] -> ShowS
Show)
searchpos :: Buffer -> [Text] -> SearchMode -> Neovim env AgdaPos
searchpos :: forall env. Buffer -> [Text] -> SearchMode -> Neovim env AgdaPos
searchpos Buffer
b [Text]
pats SearchMode
dir = do
ObjectArray [forall a. Num a => Object -> Maybe a
objectToInt @Int -> Just (Int -> Index 'Line 'OneIndexed
forall a (e :: Unit). Integral a => a -> Index e 'OneIndexed
toOneIndexed -> Index 'Line 'OneIndexed
line), forall a. Num a => Object -> Maybe a
objectToInt @Int -> Just (Int -> Index 'Byte 'ZeroIndexed
forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed -> Index 'Byte 'ZeroIndexed
col)]
<- Text -> Vector Object -> Neovim env Object
forall env. Text -> Vector Object -> Neovim env Object
vim_call_function Text
"searchpos" (Vector Object -> Neovim env Object)
-> Vector Object -> Neovim env Object
forall a b. (a -> b) -> a -> b
$ [Object] -> Vector Object
forall a. [a] -> Vector a
V.fromList
[ ByteString -> Object
ObjectString (ByteString -> Object) -> ByteString -> Object
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
encodeUtf8 (Text -> ByteString) -> Text -> ByteString
forall a b. (a -> b) -> a -> b
$ Text -> [Text] -> Text
T.intercalate Text
"\\|" [Text]
pats
, ByteString -> Object
ObjectString (ByteString -> Object) -> ByteString -> Object
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
encodeUtf8 (Text -> ByteString) -> Text -> ByteString
forall a b. (a -> b) -> a -> b
$ case SearchMode
dir of
SearchMode
Forward -> Text
"n"
SearchMode
Backward -> Text
"bn"
]
Buffer -> VimPos -> Neovim env AgdaPos
forall env. Buffer -> VimPos -> Neovim env AgdaPos
unvimify Buffer
b (Index 'Line 'ZeroIndexed -> Index 'Byte 'ZeroIndexed -> VimPos
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos (Index 'Line 'OneIndexed -> Index 'Line 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex Index 'Line 'OneIndexed
line) Index 'Byte 'ZeroIndexed
col)
setWindowCursor :: Window -> AgdaPos -> Neovim env ()
setWindowCursor :: forall env. Window -> AgdaPos -> Neovim env ()
setWindowCursor Window
w AgdaPos
p = do
Buffer
b <- Window -> Neovim env Buffer
forall env. Window -> Neovim env Buffer
window_get_buffer Window
w
Pos Index 'Line 'ZeroIndexed
l Index 'Byte 'ZeroIndexed
c <- Buffer -> AgdaPos -> Neovim env VimPos
forall env. Buffer -> AgdaPos -> Neovim env VimPos
vimify Buffer
b AgdaPos
p
Window -> (Int64, Int64) -> Neovim env ()
forall env. Window -> (Int64, Int64) -> Neovim env ()
window_set_cursor Window
w (Index 'Line 'OneIndexed -> Int64
forall a (e :: Unit). Num a => Index e 'OneIndexed -> a
fromOneIndexed (Index 'Line 'ZeroIndexed -> Index 'Line 'OneIndexed
forall (e :: Unit). Index e 'ZeroIndexed -> Index e 'OneIndexed
oneIndex Index 'Line 'ZeroIndexed
l), Index 'Byte 'ZeroIndexed -> Int64
forall a (e :: Unit). Num a => Index e 'ZeroIndexed -> a
fromZeroIndexed Index 'Byte 'ZeroIndexed
c)
replaceInterval :: Buffer -> Interval AgdaPos -> Text -> Neovim env ()
replaceInterval :: forall env. Buffer -> Interval AgdaPos -> Text -> Neovim env ()
replaceInterval Buffer
b Interval AgdaPos
ival Text
str
= do
Interval (Pos Index 'Line 'ZeroIndexed
sl Index 'Byte 'ZeroIndexed
sc) (Pos Index 'Line 'ZeroIndexed
el Index 'Byte 'ZeroIndexed
ec) <- (AgdaPos -> Neovim env VimPos)
-> Interval AgdaPos -> Neovim env (Interval VimPos)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Interval a -> f (Interval b)
traverse (Buffer -> AgdaPos -> Neovim env VimPos
forall env. Buffer -> AgdaPos -> Neovim env VimPos
vimify Buffer
b) Interval AgdaPos
ival
Buffer
-> Int64 -> Int64 -> Int64 -> Int64 -> Vector Text -> Neovim env ()
forall env.
Buffer
-> Int64 -> Int64 -> Int64 -> Int64 -> Vector Text -> Neovim env ()
nvim_buf_set_text Buffer
b (Index 'Line 'ZeroIndexed -> Int64
forall {e :: Unit}. Index e 'ZeroIndexed -> Int64
from0 Index 'Line 'ZeroIndexed
sl) (Index 'Byte 'ZeroIndexed -> Int64
forall {e :: Unit}. Index e 'ZeroIndexed -> Int64
from0 Index 'Byte 'ZeroIndexed
sc) (Index 'Line 'ZeroIndexed -> Int64
forall {e :: Unit}. Index e 'ZeroIndexed -> Int64
from0 Index 'Line 'ZeroIndexed
el) (Index 'Byte 'ZeroIndexed -> Int64
forall {e :: Unit}. Index e 'ZeroIndexed -> Int64
from0 Index 'Byte 'ZeroIndexed
ec) (Vector Text -> Neovim env ()) -> Vector Text -> Neovim env ()
forall a b. (a -> b) -> a -> b
$ [Text] -> Vector Text
forall a. [a] -> Vector a
V.fromList ([Text] -> Vector Text) -> [Text] -> Vector Text
forall a b. (a -> b) -> a -> b
$ Text -> [Text]
T.lines Text
str
where
from0 :: Index e 'ZeroIndexed -> Int64
from0 = Index e 'ZeroIndexed -> Int64
forall a (e :: Unit). Num a => Index e 'ZeroIndexed -> a
fromZeroIndexed
unvimify :: Buffer -> VimPos -> Neovim env AgdaPos
unvimify :: forall env. Buffer -> VimPos -> Neovim env AgdaPos
unvimify Buffer
b (Pos Index 'Line 'ZeroIndexed
line Index 'Byte 'ZeroIndexed
col) = do
Text
txt <- Buffer -> Index 'Line 'ZeroIndexed -> Neovim env Text
forall env. Buffer -> Index 'Line 'ZeroIndexed -> Neovim env Text
getBufferLine Buffer
b Index 'Line 'ZeroIndexed
line
let col' :: Index 'CodePoint 'ZeroIndexed
col' = HasCallStack =>
Text -> Index 'Byte 'ZeroIndexed -> Index 'CodePoint 'ZeroIndexed
Text -> Index 'Byte 'ZeroIndexed -> Index 'CodePoint 'ZeroIndexed
fromBytes Text
txt Index 'Byte 'ZeroIndexed
col
AgdaPos -> Neovim env AgdaPos
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Index 'Line 'OneIndexed -> Index 'CodePoint 'OneIndexed -> AgdaPos
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos (Index 'Line 'ZeroIndexed -> Index 'Line 'OneIndexed
forall (e :: Unit). Index e 'ZeroIndexed -> Index e 'OneIndexed
oneIndex Index 'Line 'ZeroIndexed
line) (Index 'CodePoint 'ZeroIndexed -> Index 'CodePoint 'OneIndexed
forall (e :: Unit). Index e 'ZeroIndexed -> Index e 'OneIndexed
oneIndex Index 'CodePoint 'ZeroIndexed
col'))
vimify :: Buffer -> AgdaPos -> Neovim env VimPos
vimify :: forall env. Buffer -> AgdaPos -> Neovim env VimPos
vimify Buffer
b (Pos (Index 'Line 'OneIndexed -> Index 'Line 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex -> Index 'Line 'ZeroIndexed
line) (Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex -> Index 'CodePoint 'ZeroIndexed
col)) = do
Text
txt <- Buffer -> Index 'Line 'ZeroIndexed -> Neovim env Text
forall env. Buffer -> Index 'Line 'ZeroIndexed -> Neovim env Text
getBufferLine Buffer
b Index 'Line 'ZeroIndexed
line
let col' :: Index 'Byte 'ZeroIndexed
col' = Text -> Index 'CodePoint 'ZeroIndexed -> Index 'Byte 'ZeroIndexed
toBytes Text
txt Index 'CodePoint 'ZeroIndexed
col
VimPos -> Neovim env VimPos
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Index 'Line 'ZeroIndexed -> Index 'Byte 'ZeroIndexed -> VimPos
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos Index 'Line 'ZeroIndexed
line Index 'Byte 'ZeroIndexed
col')
getIndent :: Buffer -> LineNumber 'ZeroIndexed -> Neovim env Int
getIndent :: forall env. Buffer -> Index 'Line 'ZeroIndexed -> Neovim env Int
getIndent Buffer
b Index 'Line 'ZeroIndexed
l = do
Text
txt <- Buffer -> Index 'Line 'ZeroIndexed -> Neovim env Text
forall env. Buffer -> Index 'Line 'ZeroIndexed -> Neovim env Text
getBufferLine Buffer
b Index 'Line 'ZeroIndexed
l
Int -> Neovim env Int
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Neovim env Int) -> Int -> Neovim env Int
forall a b. (a -> b) -> a -> b
$ Text -> Int
T.length (Text -> Int) -> Text -> Int
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ') Text
txt
getBufferLine :: Buffer -> LineNumber 'ZeroIndexed -> Neovim env Text
getBufferLine :: forall env. Buffer -> Index 'Line 'ZeroIndexed -> Neovim env Text
getBufferLine Buffer
b Index 'Line 'ZeroIndexed
l = Buffer -> Int64 -> Neovim env Text
forall env. Buffer -> Int64 -> Neovim env Text
buffer_get_line Buffer
b (Index 'Line 'ZeroIndexed -> Int64
forall a (e :: Unit). Num a => Index e 'ZeroIndexed -> a
fromZeroIndexed Index 'Line 'ZeroIndexed
l)
getBufferInterval :: Buffer -> Interval AgdaPos -> Neovim env Text
getBufferInterval :: forall env. Buffer -> Interval AgdaPos -> Neovim env Text
getBufferInterval Buffer
b (Interval AgdaPos
start AgdaPos
end) = do
Pos Index 'Line 'ZeroIndexed
sl Index 'Byte 'ZeroIndexed
_ <- Buffer -> AgdaPos -> Neovim env VimPos
forall env. Buffer -> AgdaPos -> Neovim env VimPos
vimify Buffer
b AgdaPos
start
Pos Index 'Line 'ZeroIndexed
el Index 'Byte 'ZeroIndexed
_ <- Buffer -> AgdaPos -> Neovim env VimPos
forall env. Buffer -> AgdaPos -> Neovim env VimPos
vimify Buffer
b AgdaPos
end
[Text]
ls <- (Vector Text -> [Text])
-> Neovim env (Vector Text) -> Neovim env [Text]
forall a b. (a -> b) -> Neovim env a -> Neovim env b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Vector Text -> [Text]
forall a. Vector a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Neovim env (Vector Text) -> Neovim env [Text])
-> Neovim env (Vector Text) -> Neovim env [Text]
forall a b. (a -> b) -> a -> b
$ Buffer -> Int64 -> Int64 -> Bool -> Neovim env (Vector Text)
forall env.
Buffer -> Int64 -> Int64 -> Bool -> Neovim env (Vector Text)
nvim_buf_get_lines Buffer
b (Index 'Line 'ZeroIndexed -> Int64
forall {e :: Unit}. Index e 'ZeroIndexed -> Int64
from0 Index 'Line 'ZeroIndexed
sl) (Index 'Line 'ZeroIndexed -> Int64
forall {e :: Unit}. Index e 'ZeroIndexed -> Int64
from0 Index 'Line 'ZeroIndexed
el Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int64
1) Bool
False
Text -> Neovim env Text
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Neovim env Text) -> Text -> Neovim env Text
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$
[Text]
ls [Text] -> ([Text] -> [Text]) -> [Text]
forall a b. a -> (a -> b) -> b
& (Text -> Identity Text) -> [Text] -> Identity [Text]
forall s a. Snoc s s a a => Traversal' s a
Traversal' [Text] Text
_last ((Text -> Identity Text) -> [Text] -> Identity [Text])
-> (Text -> Text) -> [Text] -> [Text]
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Int -> Text -> Text
T.take (Index 'CodePoint 'OneIndexed -> Int
forall {e :: Unit}. Index e 'OneIndexed -> Int
from1 (AgdaPos -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index e j
p_col AgdaPos
end))
[Text] -> ([Text] -> [Text]) -> [Text]
forall a b. a -> (a -> b) -> b
& (Text -> Identity Text) -> [Text] -> Identity [Text]
forall s a. Cons s s a a => Traversal' s a
Traversal' [Text] Text
_head ((Text -> Identity Text) -> [Text] -> Identity [Text])
-> (Text -> Text) -> [Text] -> [Text]
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Int -> Text -> Text
T.drop (Index 'CodePoint 'OneIndexed -> Int
forall {e :: Unit}. Index e 'OneIndexed -> Int
from1 (AgdaPos -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index e j
p_col AgdaPos
start))
where
from0 :: Index e 'ZeroIndexed -> Int64
from0 = Index e 'ZeroIndexed -> Int64
forall a (e :: Unit). Num a => Index e 'ZeroIndexed -> a
fromZeroIndexed
from1 :: Index e 'OneIndexed -> Int
from1 = Index e 'ZeroIndexed -> Int
forall a (e :: Unit). Num a => Index e 'ZeroIndexed -> a
fromZeroIndexed (Index e 'ZeroIndexed -> Int)
-> (Index e 'OneIndexed -> Index e 'ZeroIndexed)
-> Index e 'OneIndexed
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index e 'OneIndexed -> Index e 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex
reportError :: Text -> Neovim env ()
reportError :: forall env. Text -> Neovim env ()
reportError = Text -> Neovim env ()
forall env. Text -> Neovim env ()
vim_report_error
reportInfo :: Text -> Neovim env ()
reportInfo :: forall env. Text -> Neovim env ()
reportInfo Text
m = Text -> Neovim env ()
forall env. Text -> Neovim env ()
vim_out_write (Text -> Neovim env ()) -> Text -> Neovim env ()
forall a b. (a -> b) -> a -> b
$ Text
m Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n"
setreg :: Text -> Text -> Neovim env ()
setreg :: forall env. Text -> Text -> Neovim env ()
setreg Text
reg Text
val
= Neovim env Object -> Neovim env ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void
(Neovim env Object -> Neovim env ())
-> Neovim env Object -> Neovim env ()
forall a b. (a -> b) -> a -> b
$ Text -> Vector Object -> Neovim env Object
forall env. Text -> Vector Object -> Neovim env Object
vim_call_function Text
"setreg"
(Vector Object -> Neovim env Object)
-> Vector Object -> Neovim env Object
forall a b. (a -> b) -> a -> b
$ [Object] -> Vector Object
forall a. [a] -> Vector a
V.fromList
[ ByteString -> Object
ObjectString (ByteString -> Object) -> ByteString -> Object
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
encodeUtf8 Text
reg
, ByteString -> Object
ObjectString (ByteString -> Object) -> ByteString -> Object
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
encodeUtf8 Text
val
]
getExtmarkIntervalById :: Int64 -> Buffer -> Extmark -> Neovim env (Maybe AgdaInterval)
getExtmarkIntervalById :: forall env.
Int64 -> Buffer -> Extmark -> Neovim env (Maybe (Interval AgdaPos))
getExtmarkIntervalById Int64
ns Buffer
b (Extmark Int64
x) = do
Object
res
<- Text -> Vector Object -> Neovim env Object
forall env. Text -> Vector Object -> Neovim env Object
nvim_call_function Text
"nvim_buf_get_extmark_by_id"
(Vector Object -> Neovim env Object)
-> Vector Object -> Neovim env Object
forall a b. (a -> b) -> a -> b
$ [Object] -> Vector Object
forall a. [a] -> Vector a
V.fromList
([Object] -> Vector Object) -> [Object] -> Vector Object
forall a b. (a -> b) -> a -> b
$ Buffer
b Buffer -> [Object] -> [Object]
forall o. NvimObject o => o -> [Object] -> [Object]
+: Int64
ns Int64 -> [Object] -> [Object]
forall o. NvimObject o => o -> [Object] -> [Object]
+: Int64
x Int64 -> [Object] -> [Object]
forall o. NvimObject o => o -> [Object] -> [Object]
+: forall k a. k -> a -> Map k a
M.singleton @Text Text
"details" Bool
True Map Text Bool -> [Object] -> [Object]
forall o. NvimObject o => o -> [Object] -> [Object]
+: []
case Object
res of
ObjectArray [ forall a. Num a => Object -> Maybe a
objectToInt @Int -> Just (Int -> Index 'Line 'ZeroIndexed
forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed -> Index 'Line 'ZeroIndexed
sline)
, forall a. Num a => Object -> Maybe a
objectToInt @Int -> Just (Int -> Index 'Byte 'ZeroIndexed
forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed -> Index 'Byte 'ZeroIndexed
scol)
, ObjectMap Map Object Object
details
] -> do
let toZ :: Object -> Maybe (Index e 'ZeroIndexed)
toZ = (Int -> Index e 'ZeroIndexed)
-> Maybe Int -> Maybe (Index e 'ZeroIndexed)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Index e 'ZeroIndexed
forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed (Maybe Int -> Maybe (Index e 'ZeroIndexed))
-> (Object -> Maybe Int) -> Object -> Maybe (Index e 'ZeroIndexed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Object -> Maybe a
objectToInt @Int
Just Index e 'ZeroIndexed
eline = Object -> Maybe (Index e 'ZeroIndexed)
forall {e :: Unit}. Object -> Maybe (Index e 'ZeroIndexed)
toZ (Object -> Maybe (Index e 'ZeroIndexed))
-> Object -> Maybe (Index e 'ZeroIndexed)
forall a b. (a -> b) -> a -> b
$ Map Object Object
details Map Object Object -> Object -> Object
forall k a. Ord k => Map k a -> k -> a
M.! ByteString -> Object
ObjectString ByteString
"end_row"
Just Index e 'ZeroIndexed
ecol = Object -> Maybe (Index e 'ZeroIndexed)
forall {e :: Unit}. Object -> Maybe (Index e 'ZeroIndexed)
toZ (Object -> Maybe (Index e 'ZeroIndexed))
-> Object -> Maybe (Index e 'ZeroIndexed)
forall a b. (a -> b) -> a -> b
$ Map Object Object
details Map Object Object -> Object -> Object
forall k a. Ord k => Map k a -> k -> a
M.! ByteString -> Object
ObjectString ByteString
"end_col"
(Interval AgdaPos -> Maybe (Interval AgdaPos))
-> Neovim env (Interval AgdaPos)
-> Neovim env (Maybe (Interval AgdaPos))
forall a b. (a -> b) -> Neovim env a -> Neovim env b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Interval AgdaPos -> Maybe (Interval AgdaPos)
forall a. a -> Maybe a
Just (Neovim env (Interval AgdaPos)
-> Neovim env (Maybe (Interval AgdaPos)))
-> Neovim env (Interval AgdaPos)
-> Neovim env (Maybe (Interval AgdaPos))
forall a b. (a -> b) -> a -> b
$ (VimPos -> Neovim env AgdaPos)
-> Interval VimPos -> Neovim env (Interval AgdaPos)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Interval a -> f (Interval b)
traverse (Buffer -> VimPos -> Neovim env AgdaPos
forall env. Buffer -> VimPos -> Neovim env AgdaPos
unvimify Buffer
b) (Interval VimPos -> Neovim env (Interval AgdaPos))
-> Interval VimPos -> Neovim env (Interval AgdaPos)
forall a b. (a -> b) -> a -> b
$ VimPos -> VimPos -> Interval VimPos
forall p. p -> p -> Interval p
Interval (Index 'Line 'ZeroIndexed -> Index 'Byte 'ZeroIndexed -> VimPos
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos Index 'Line 'ZeroIndexed
sline Index 'Byte 'ZeroIndexed
scol) (VimPos -> Interval VimPos) -> VimPos -> Interval VimPos
forall a b. (a -> b) -> a -> b
$ Index 'Line 'ZeroIndexed -> Index 'Byte 'ZeroIndexed -> VimPos
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos Index 'Line 'ZeroIndexed
forall {e :: Unit}. Index e 'ZeroIndexed
eline Index 'Byte 'ZeroIndexed
forall {e :: Unit}. Index e 'ZeroIndexed
ecol
Object
_ -> Maybe (Interval AgdaPos) -> Neovim env (Maybe (Interval AgdaPos))
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Interval AgdaPos)
forall a. Maybe a
Nothing
getSurroundingMotion
:: Window
-> Buffer
-> Text
-> AgdaPos
-> Neovim env (AgdaPos, AgdaPos)
getSurroundingMotion :: forall env.
Window
-> Buffer -> Text -> AgdaPos -> Neovim env (AgdaPos, AgdaPos)
getSurroundingMotion Window
w Buffer
b Text
motion AgdaPos
p = do
Neovim env (AgdaPos, AgdaPos) -> Neovim env (AgdaPos, AgdaPos)
forall env a. Neovim env a -> Neovim env a
savingCurrentWindow (Neovim env (AgdaPos, AgdaPos) -> Neovim env (AgdaPos, AgdaPos))
-> Neovim env (AgdaPos, AgdaPos) -> Neovim env (AgdaPos, AgdaPos)
forall a b. (a -> b) -> a -> b
$ do
Window
-> Neovim env (AgdaPos, AgdaPos) -> Neovim env (AgdaPos, AgdaPos)
forall env a. Window -> Neovim env a -> Neovim env a
savingCurrentPosition Window
w (Neovim env (AgdaPos, AgdaPos) -> Neovim env (AgdaPos, AgdaPos))
-> Neovim env (AgdaPos, AgdaPos) -> Neovim env (AgdaPos, AgdaPos)
forall a b. (a -> b) -> a -> b
$ do
Window -> Neovim env ()
forall env. Window -> Neovim env ()
nvim_set_current_win Window
w
Window -> AgdaPos -> Neovim env ()
forall env. Window -> AgdaPos -> Neovim env ()
setWindowCursor Window
w AgdaPos
p
Text -> Neovim env ()
forall env. Text -> Neovim env ()
vim_command (Text -> Neovim env ()) -> Text -> Neovim env ()
forall a b. (a -> b) -> a -> b
$ Text
"normal v" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
motion
AgdaPos
start <- Buffer -> Char -> Neovim env AgdaPos
forall env. Buffer -> Char -> Neovim env AgdaPos
getpos Buffer
b Char
'v'
AgdaPos
end <- Buffer -> Char -> Neovim env AgdaPos
forall env. Buffer -> Char -> Neovim env AgdaPos
getpos Buffer
b Char
'.'
Neovim env Int64 -> Neovim env ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim env Int64 -> Neovim env ())
-> Neovim env Int64 -> Neovim env ()
forall a b. (a -> b) -> a -> b
$ Text -> Neovim env Int64
forall env. Text -> Neovim env Int64
nvim_input Text
"<esc>"
(AgdaPos, AgdaPos) -> Neovim env (AgdaPos, AgdaPos)
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AgdaPos
start, AgdaPos
end)
getLambdaClause
:: Window
-> Buffer
-> AgdaInterval
-> Neovim env AgdaInterval
getLambdaClause :: forall env.
Window
-> Buffer -> Interval AgdaPos -> Neovim env (Interval AgdaPos)
getLambdaClause Window
w Buffer
b (Interval AgdaPos
p0 AgdaPos
p1) = do
Neovim env (Interval AgdaPos) -> Neovim env (Interval AgdaPos)
forall env a. Neovim env a -> Neovim env a
savingCurrentWindow (Neovim env (Interval AgdaPos) -> Neovim env (Interval AgdaPos))
-> Neovim env (Interval AgdaPos) -> Neovim env (Interval AgdaPos)
forall a b. (a -> b) -> a -> b
$ do
Window
-> Neovim env (Interval AgdaPos) -> Neovim env (Interval AgdaPos)
forall env a. Window -> Neovim env a -> Neovim env a
savingCurrentPosition Window
w (Neovim env (Interval AgdaPos) -> Neovim env (Interval AgdaPos))
-> Neovim env (Interval AgdaPos) -> Neovim env (Interval AgdaPos)
forall a b. (a -> b) -> a -> b
$ do
Window -> Neovim env ()
forall env. Window -> Neovim env ()
nvim_set_current_win Window
w
Window -> AgdaPos -> Neovim env ()
forall env. Window -> AgdaPos -> Neovim env ()
setWindowCursor Window
w AgdaPos
p0
AgdaPos
start <- Buffer -> [Text] -> SearchMode -> Neovim env AgdaPos
forall env. Buffer -> [Text] -> SearchMode -> Neovim env AgdaPos
searchpos Buffer
b [Text
"{", Text
";"] SearchMode
Backward
Window -> AgdaPos -> Neovim env ()
forall env. Window -> AgdaPos -> Neovim env ()
setWindowCursor Window
w AgdaPos
p1
AgdaPos
end <- Buffer -> [Text] -> SearchMode -> Neovim env AgdaPos
forall env. Buffer -> [Text] -> SearchMode -> Neovim env AgdaPos
searchpos Buffer
b [Text
";", Text
"}"] SearchMode
Forward
Interval AgdaPos -> Neovim env (Interval AgdaPos)
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AgdaPos -> AgdaPos -> Interval AgdaPos
forall p. p -> p -> Interval p
Interval AgdaPos
start AgdaPos
end)