{-# LANGUAGE CPP #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE OverloadedLabels   #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeApplications #-}

module Cornelis.Highlighting where

import           Control.Lens ((<>~), (.~))
import           Control.Monad.Trans (lift)
import           Control.Monad.Trans.Maybe
import           Cornelis.Diff
import           Cornelis.Offsets
import           Cornelis.Pretty
import           Cornelis.Types
import           Cornelis.Utils
import           Cornelis.Vim (unvimify, vimify)
import           Data.Coerce (coerce)
import           Data.IntervalMap.FingerTree (IntervalMap)
import qualified Data.IntervalMap.FingerTree as IM
import qualified Data.Map as M
import           Data.Maybe (listToMaybe, catMaybes, mapMaybe)
import qualified Data.Text as T
import           Data.Text.Encoding (encodeUtf8)
import           Data.Traversable (for)
import           Data.Vector (Vector)
import qualified Data.Vector as V
import           Neovim
import           Neovim.API.Text

lineIntervalsForBuffer :: Buffer -> Neovim CornelisEnv LineIntervals
lineIntervalsForBuffer :: Buffer -> Neovim CornelisEnv LineIntervals
lineIntervalsForBuffer Buffer
b = do
  Vector Text
buf_lines <- Buffer
-> Int64 -> Int64 -> Bool -> Neovim CornelisEnv (Vector Text)
forall env.
Buffer -> Int64 -> Int64 -> Bool -> Neovim env (Vector Text)
nvim_buf_get_lines Buffer
b Int64
0 (-Int64
1) Bool
True
  LineIntervals -> Neovim CornelisEnv LineIntervals
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LineIntervals -> Neovim CornelisEnv LineIntervals)
-> LineIntervals -> Neovim CornelisEnv LineIntervals
forall a b. (a -> b) -> a -> b
$ Vector Text -> LineIntervals
getLineIntervals Vector Text
buf_lines

updateLineIntervals :: Buffer -> Neovim CornelisEnv ()
updateLineIntervals :: Buffer -> Neovim CornelisEnv ()
updateLineIntervals Buffer
b = do
  LineIntervals
li <- Buffer -> Neovim CornelisEnv LineIntervals
lineIntervalsForBuffer Buffer
b
  Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
modifyBufferStuff Buffer
b ((BufferStuff -> BufferStuff) -> Neovim CornelisEnv ())
-> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ ASetter BufferStuff BufferStuff LineIntervals LineIntervals
#bs_code_map ASetter BufferStuff BufferStuff LineIntervals LineIntervals
-> LineIntervals -> BufferStuff -> BufferStuff
forall s t a b. ASetter s t a b -> b -> s -> t
.~ LineIntervals
li

highlightBuffer :: Buffer -> [Highlight] -> Neovim CornelisEnv (M.Map AgdaInterval Extmark)
highlightBuffer :: Buffer
-> [Highlight] -> Neovim CornelisEnv (Map AgdaInterval Extmark)
highlightBuffer Buffer
b [Highlight]
hs = Buffer
-> (BufferStuff -> Neovim CornelisEnv (Map AgdaInterval Extmark))
-> Neovim CornelisEnv (Map AgdaInterval Extmark)
forall a.
Monoid a =>
Buffer
-> (BufferStuff -> Neovim CornelisEnv a) -> Neovim CornelisEnv a
withBufferStuff Buffer
b ((BufferStuff -> Neovim CornelisEnv (Map AgdaInterval Extmark))
 -> Neovim CornelisEnv (Map AgdaInterval Extmark))
-> (BufferStuff -> Neovim CornelisEnv (Map AgdaInterval Extmark))
-> Neovim CornelisEnv (Map AgdaInterval Extmark)
forall a b. (a -> b) -> a -> b
$ \BufferStuff
bs -> do
  let li :: LineIntervals
li = BufferStuff -> LineIntervals
bs_code_map BufferStuff
bs
  ([Map AgdaInterval Extmark]
holes, [(Highlight, Maybe Extmark)]
exts) <- ([(Map AgdaInterval Extmark, (Highlight, Maybe Extmark))]
 -> ([Map AgdaInterval Extmark], [(Highlight, Maybe Extmark)]))
-> Neovim
     CornelisEnv
     [(Map AgdaInterval Extmark, (Highlight, Maybe Extmark))]
-> Neovim
     CornelisEnv
     ([Map AgdaInterval Extmark], [(Highlight, Maybe Extmark)])
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Map AgdaInterval Extmark, (Highlight, Maybe Extmark))]
-> ([Map AgdaInterval Extmark], [(Highlight, Maybe Extmark)])
forall a b. [(a, b)] -> ([a], [b])
unzip (Neovim
   CornelisEnv
   [(Map AgdaInterval Extmark, (Highlight, Maybe Extmark))]
 -> Neovim
      CornelisEnv
      ([Map AgdaInterval Extmark], [(Highlight, Maybe Extmark)]))
-> Neovim
     CornelisEnv
     [(Map AgdaInterval Extmark, (Highlight, Maybe Extmark))]
-> Neovim
     CornelisEnv
     ([Map AgdaInterval Extmark], [(Highlight, Maybe Extmark)])
forall a b. (a -> b) -> a -> b
$ [Highlight]
-> (Highlight
    -> Neovim
         CornelisEnv (Map AgdaInterval Extmark, (Highlight, Maybe Extmark)))
-> Neovim
     CornelisEnv
     [(Map AgdaInterval Extmark, (Highlight, Maybe Extmark))]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Highlight]
hs ((Highlight
  -> Neovim
       CornelisEnv (Map AgdaInterval Extmark, (Highlight, Maybe Extmark)))
 -> Neovim
      CornelisEnv
      [(Map AgdaInterval Extmark, (Highlight, Maybe Extmark))])
-> (Highlight
    -> Neovim
         CornelisEnv (Map AgdaInterval Extmark, (Highlight, Maybe Extmark)))
-> Neovim
     CornelisEnv
     [(Map AgdaInterval Extmark, (Highlight, Maybe Extmark))]
forall a b. (a -> b) -> a -> b
$ \Highlight
hl -> do
    (Map AgdaInterval Extmark
hole, Maybe Extmark
mext) <- Buffer
-> LineIntervals
-> Highlight
-> Neovim CornelisEnv (Map AgdaInterval Extmark, Maybe Extmark)
addHighlight Buffer
b LineIntervals
li Highlight
hl
    (Map AgdaInterval Extmark, (Highlight, Maybe Extmark))
-> Neovim
     CornelisEnv (Map AgdaInterval Extmark, (Highlight, Maybe Extmark))
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map AgdaInterval Extmark
hole, (Highlight
hl, Maybe Extmark
mext))

  let zs :: [(Extmark, DefinitionSite)]
zs = [Maybe (Extmark, DefinitionSite)] -> [(Extmark, DefinitionSite)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Extmark, DefinitionSite)] -> [(Extmark, DefinitionSite)])
-> [Maybe (Extmark, DefinitionSite)] -> [(Extmark, DefinitionSite)]
forall a b. (a -> b) -> a -> b
$ do
        (Highlight
hl, Maybe Extmark
mext) <- [(Highlight, Maybe Extmark)]
exts
        Maybe (Extmark, DefinitionSite)
-> [Maybe (Extmark, DefinitionSite)]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Extmark, DefinitionSite)
 -> [Maybe (Extmark, DefinitionSite)])
-> Maybe (Extmark, DefinitionSite)
-> [Maybe (Extmark, DefinitionSite)]
forall a b. (a -> b) -> a -> b
$ do
          Extmark
ext <- Maybe Extmark
mext
          DefinitionSite
ds <- Highlight -> Maybe DefinitionSite
hl_definitionSite Highlight
hl
          (Extmark, DefinitionSite) -> Maybe (Extmark, DefinitionSite)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Extmark
ext, DefinitionSite
ds)

  Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
modifyBufferStuff Buffer
b ((BufferStuff -> BufferStuff) -> Neovim CornelisEnv ())
-> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ ASetter
  BufferStuff
  BufferStuff
  (Map Extmark DefinitionSite)
  (Map Extmark DefinitionSite)
#bs_goto_sites ASetter
  BufferStuff
  BufferStuff
  (Map Extmark DefinitionSite)
  (Map Extmark DefinitionSite)
-> Map Extmark DefinitionSite -> BufferStuff -> BufferStuff
forall a s t. Semigroup a => ASetter s t a a -> a -> s -> t
<>~ [(Extmark, DefinitionSite)] -> Map Extmark DefinitionSite
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Extmark, DefinitionSite)]
zs
  Map AgdaInterval Extmark
-> Neovim CornelisEnv (Map AgdaInterval Extmark)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map AgdaInterval Extmark
 -> Neovim CornelisEnv (Map AgdaInterval Extmark))
-> Map AgdaInterval Extmark
-> Neovim CornelisEnv (Map AgdaInterval Extmark)
forall a b. (a -> b) -> a -> b
$ [Map AgdaInterval Extmark] -> Map AgdaInterval Extmark
forall a. Monoid a => [a] -> a
mconcat [Map AgdaInterval Extmark]
holes

getLineIntervals :: Vector Text -> LineIntervals
getLineIntervals :: Vector Text -> LineIntervals
getLineIntervals = IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
-> LineIntervals
LineIntervals (IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
 -> LineIntervals)
-> (Vector Text
    -> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text))
-> Vector Text
-> LineIntervals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AgdaIndex
-> LineNumber 'ZeroIndexed
-> Vector Text
-> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
go (forall a (e :: Unit). Integral a => a -> Index e 'OneIndexed
toOneIndexed @Int Int
1) (forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed @Int Int
0)
  where
    go
        :: AgdaIndex
        -> LineNumber 'ZeroIndexed
        -> Vector Text
        -> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
    go :: AgdaIndex
-> LineNumber 'ZeroIndexed
-> Vector Text
-> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
go AgdaIndex
pos LineNumber 'ZeroIndexed
line Vector Text
v
      | Just (Text
t, Vector Text
ss) <- Vector Text -> Maybe (Text, Vector Text)
forall a. Vector a -> Maybe (a, Vector a)
V.uncons Vector Text
v =
        let len :: Int
len = Text -> Int
T.length Text
t
            pos' :: AgdaIndex
pos' = AgdaIndex
pos AgdaIndex -> Offset 'CodePoint -> AgdaIndex
forall (e :: Unit) (i :: Indexing).
Index e i -> Offset e -> Index e i
.+ Int -> Offset 'CodePoint
forall (e :: Unit). Int -> Offset e
Offset Int
len
        in Interval AgdaIndex
-> (LineNumber 'ZeroIndexed, Text)
-> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
-> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
forall v a.
Ord v =>
Interval v -> a -> IntervalMap v a -> IntervalMap v a
IM.insert (AgdaIndex -> AgdaIndex -> Interval AgdaIndex
forall v. v -> v -> Interval v
IM.Interval AgdaIndex
pos AgdaIndex
pos') (LineNumber 'ZeroIndexed
line, Text
t)
              (IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
 -> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text))
-> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
-> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
forall a b. (a -> b) -> a -> b
$ AgdaIndex
-> LineNumber 'ZeroIndexed
-> Vector Text
-> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
go (AgdaIndex -> AgdaIndex
forall (e :: Unit) (i :: Indexing). Index e i -> Index e i
incIndex AgdaIndex
pos') (LineNumber 'ZeroIndexed -> LineNumber 'ZeroIndexed
forall (e :: Unit) (i :: Indexing). Index e i -> Index e i
incIndex LineNumber 'ZeroIndexed
line) Vector Text
ss
      | Bool
otherwise = IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
forall a. Monoid a => a
mempty

lookupPoint :: LineIntervals -> AgdaIndex -> Maybe VimPos
lookupPoint :: LineIntervals -> AgdaIndex -> Maybe VimPos
lookupPoint (LineIntervals IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
im) AgdaIndex
i = do
  (IM.Interval AgdaIndex
lineStart AgdaIndex
_, (LineNumber 'ZeroIndexed
line, Text
s)) <- [(Interval AgdaIndex, (LineNumber 'ZeroIndexed, Text))]
-> Maybe (Interval AgdaIndex, (LineNumber 'ZeroIndexed, Text))
forall a. [a] -> Maybe a
listToMaybe ([(Interval AgdaIndex, (LineNumber 'ZeroIndexed, Text))]
 -> Maybe (Interval AgdaIndex, (LineNumber 'ZeroIndexed, Text)))
-> [(Interval AgdaIndex, (LineNumber 'ZeroIndexed, Text))]
-> Maybe (Interval AgdaIndex, (LineNumber 'ZeroIndexed, Text))
forall a b. (a -> b) -> a -> b
$ AgdaIndex
-> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
-> [(Interval AgdaIndex, (LineNumber 'ZeroIndexed, Text))]
forall v a. Ord v => v -> IntervalMap v a -> [(Interval v, a)]
IM.search AgdaIndex
i IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
im
  let col :: Index 'Byte 'ZeroIndexed
col = Text -> Index 'CodePoint 'ZeroIndexed -> Index 'Byte 'ZeroIndexed
toBytes Text
s (forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed @Int Int
0 Index 'CodePoint 'ZeroIndexed
-> Offset 'CodePoint -> Index 'CodePoint 'ZeroIndexed
forall (e :: Unit) (i :: Indexing).
Index e i -> Offset e -> Index e i
.+ (AgdaIndex
i AgdaIndex -> AgdaIndex -> Offset 'CodePoint
forall (e :: Unit) (i :: Indexing).
Index e i -> Index e i -> Offset e
.-. AgdaIndex
lineStart))
  VimPos -> Maybe VimPos
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LineNumber 'ZeroIndexed -> Index 'Byte 'ZeroIndexed -> VimPos
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos LineNumber 'ZeroIndexed
line Index 'Byte 'ZeroIndexed
col)

------------------------------------------------------------------------------
-- | Returns any holes it tried to highlight on the left
addHighlight
    :: Buffer
    -> LineIntervals
    -> Highlight
    -> Neovim CornelisEnv (M.Map AgdaInterval Extmark, Maybe Extmark)
addHighlight :: Buffer
-> LineIntervals
-> Highlight
-> Neovim CornelisEnv (Map AgdaInterval Extmark, Maybe Extmark)
addHighlight Buffer
b LineIntervals
lis Highlight
hl = do
  case VimPos -> VimPos -> Interval VimPos
forall p. p -> p -> Interval p
Interval
           (VimPos -> VimPos -> Interval VimPos)
-> Maybe VimPos -> Maybe (VimPos -> Interval VimPos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LineIntervals -> AgdaIndex -> Maybe VimPos
lookupPoint LineIntervals
lis (Highlight -> AgdaIndex
hl_start Highlight
hl)
           Maybe (VimPos -> Interval VimPos)
-> Maybe VimPos -> Maybe (Interval VimPos)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> LineIntervals -> AgdaIndex -> Maybe VimPos
lookupPoint LineIntervals
lis (Highlight -> AgdaIndex
hl_end Highlight
hl) of
    Just int :: Interval VimPos
int@(Interval VimPos
start VimPos
end) -> do
      Maybe Extmark
ext <- Buffer
-> Interval VimPos
-> Maybe HighlightGroup
-> Neovim CornelisEnv (Maybe Extmark)
setHighlight Buffer
b Interval VimPos
int (Maybe HighlightGroup -> Neovim CornelisEnv (Maybe Extmark))
-> Maybe HighlightGroup -> Neovim CornelisEnv (Maybe Extmark)
forall a b. (a -> b) -> a -> b
$ Highlight -> Maybe HighlightGroup
parseHighlightGroup Highlight
hl

      (Map AgdaInterval Extmark
 -> (Map AgdaInterval Extmark, Maybe Extmark))
-> Neovim CornelisEnv (Map AgdaInterval Extmark)
-> Neovim CornelisEnv (Map AgdaInterval Extmark, Maybe Extmark)
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (, Maybe Extmark
ext) (Neovim CornelisEnv (Map AgdaInterval Extmark)
 -> Neovim CornelisEnv (Map AgdaInterval Extmark, Maybe Extmark))
-> Neovim CornelisEnv (Map AgdaInterval Extmark)
-> Neovim CornelisEnv (Map AgdaInterval Extmark, Maybe Extmark)
forall a b. (a -> b) -> a -> b
$ case Highlight -> Bool
isHole Highlight
hl of
        Bool
False -> Map AgdaInterval Extmark
-> Neovim CornelisEnv (Map AgdaInterval Extmark)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map AgdaInterval Extmark
forall a. Monoid a => a
mempty
        Bool
True -> do
          let vint :: Interval VimPos
vint = VimPos -> VimPos -> Interval VimPos
forall p. p -> p -> Interval p
Interval VimPos
start VimPos
end
          AgdaInterval
aint <- (VimPos -> Neovim CornelisEnv AgdaPos)
-> Interval VimPos -> Neovim CornelisEnv AgdaInterval
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 CornelisEnv AgdaPos
forall env. Buffer -> VimPos -> Neovim env AgdaPos
unvimify Buffer
b) Interval VimPos
vint
          Map AgdaInterval Extmark
-> Neovim CornelisEnv (Map AgdaInterval Extmark)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map AgdaInterval Extmark
 -> Neovim CornelisEnv (Map AgdaInterval Extmark))
-> Map AgdaInterval Extmark
-> Neovim CornelisEnv (Map AgdaInterval Extmark)
forall a b. (a -> b) -> a -> b
$ Map AgdaInterval Extmark
-> (Extmark -> Map AgdaInterval Extmark)
-> Maybe Extmark
-> Map AgdaInterval Extmark
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map AgdaInterval Extmark
forall a. Monoid a => a
mempty (AgdaInterval -> Extmark -> Map AgdaInterval Extmark
forall k a. k -> a -> Map k a
M.singleton AgdaInterval
aint) Maybe Extmark
ext
    Maybe (Interval VimPos)
Nothing -> (Map AgdaInterval Extmark, Maybe Extmark)
-> Neovim CornelisEnv (Map AgdaInterval Extmark, Maybe Extmark)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map AgdaInterval Extmark
forall a. Monoid a => a
mempty, Maybe Extmark
forall a. Maybe a
Nothing)
  where
    -- Convert the first atom in a reply to a custom highlight
    -- group, and return whether it is a hole or not.
    --
    -- Note that Agda returns both "aspects" for regular syntax
    -- and "other aspects" for error messages, warnings and hints.
    -- Currently, the latter kind takes precedence, since it is
    -- located first in the message returned by Agda.
    --
    -- See 'Cornelis.Pretty.HighlightGroup' for more details.
    --
    -- TODO: Investigate whether is is possible/feasible to
    -- attach multiple HL groups to buffer locations.
    parseHighlightGroup :: Highlight -> Maybe HighlightGroup
    parseHighlightGroup :: Highlight -> Maybe HighlightGroup
parseHighlightGroup = [HighlightGroup] -> Maybe HighlightGroup
forall a. [a] -> Maybe a
listToMaybe ([HighlightGroup] -> Maybe HighlightGroup)
-> (Highlight -> [HighlightGroup])
-> Highlight
-> Maybe HighlightGroup
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Maybe HighlightGroup) -> [Text] -> [HighlightGroup]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Text -> Maybe HighlightGroup
atomToHlGroup ([Text] -> [HighlightGroup])
-> (Highlight -> [Text]) -> Highlight -> [HighlightGroup]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Highlight -> [Text]
hl_atoms

    isHole :: Highlight -> Bool
    isHole :: Highlight -> Bool
isHole = Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Text
"hole" ([Text] -> Bool) -> (Highlight -> [Text]) -> Highlight -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Highlight -> [Text]
hl_atoms

setHighlight
    :: Buffer
    -> Interval VimPos
    -> Maybe HighlightGroup
    -> Neovim CornelisEnv (Maybe Extmark)
setHighlight :: Buffer
-> Interval VimPos
-> Maybe HighlightGroup
-> Neovim CornelisEnv (Maybe Extmark)
setHighlight Buffer
b Interval VimPos
i Maybe HighlightGroup
hl = do
  Int64
bn <- Buffer -> Neovim CornelisEnv Int64
forall env. Buffer -> Neovim env Int64
buffer_get_number Buffer
b
  Maybe (Interval VimPos)
mi' <- Int64
-> Interval VimPos -> Neovim CornelisEnv (Maybe (Interval VimPos))
translateInterval Int64
bn Interval VimPos
i
  case Maybe (Interval VimPos)
mi' of
    Just Interval VimPos
i' -> Buffer
-> Interval VimPos
-> Maybe HighlightGroup
-> Neovim CornelisEnv (Maybe Extmark)
setHighlight' Buffer
b Interval VimPos
i' Maybe HighlightGroup
hl
    Maybe (Interval VimPos)
Nothing -> Maybe Extmark -> Neovim CornelisEnv (Maybe Extmark)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Extmark
forall a. Maybe a
Nothing

setHighlight'
    :: Buffer
    -> Interval VimPos
    -> Maybe HighlightGroup
    -> Neovim CornelisEnv (Maybe Extmark)
setHighlight' :: Buffer
-> Interval VimPos
-> Maybe HighlightGroup
-> Neovim CornelisEnv (Maybe Extmark)
setHighlight' Buffer
b (Interval (Pos LineNumber 'ZeroIndexed
sl Index 'Byte 'ZeroIndexed
sc) (Pos LineNumber 'ZeroIndexed
el Index 'Byte 'ZeroIndexed
ec)) Maybe HighlightGroup
hl = do
  Int64
ns <- (CornelisEnv -> Int64) -> Neovim CornelisEnv Int64
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CornelisEnv -> Int64
ce_namespace
  let from0 :: Index e 'ZeroIndexed -> Int64
from0 = Index e 'ZeroIndexed -> Int64
forall a (e :: Unit). Num a => Index e 'ZeroIndexed -> a
fromZeroIndexed
  (Neovim CornelisEnv (Maybe Extmark)
 -> (NeovimException -> Neovim CornelisEnv (Maybe Extmark))
 -> Neovim CornelisEnv (Maybe Extmark))
-> (NeovimException -> Neovim CornelisEnv (Maybe Extmark))
-> Neovim CornelisEnv (Maybe Extmark)
-> Neovim CornelisEnv (Maybe Extmark)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Neovim CornelisEnv (Maybe Extmark)
-> (NeovimException -> Neovim CornelisEnv (Maybe Extmark))
-> Neovim CornelisEnv (Maybe Extmark)
forall (io :: * -> *) a.
MonadUnliftIO io =>
io a -> (NeovimException -> io a) -> io a
catchNeovimException (Neovim CornelisEnv (Maybe Extmark)
-> NeovimException -> Neovim CornelisEnv (Maybe Extmark)
forall a b. a -> b -> a
const (Maybe Extmark -> Neovim CornelisEnv (Maybe Extmark)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Extmark
forall a. Maybe a
Nothing))
    (Neovim CornelisEnv (Maybe Extmark)
 -> Neovim CornelisEnv (Maybe Extmark))
-> Neovim CornelisEnv (Maybe Extmark)
-> Neovim CornelisEnv (Maybe Extmark)
forall a b. (a -> b) -> a -> b
$ (Int64 -> Maybe Extmark)
-> Neovim CornelisEnv Int64 -> Neovim CornelisEnv (Maybe Extmark)
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Extmark -> Maybe Extmark
forall a. a -> Maybe a
Just (Extmark -> Maybe Extmark)
-> (Int64 -> Extmark) -> Int64 -> Maybe Extmark
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Extmark
forall a b. Coercible a b => a -> b
coerce)
    (Neovim CornelisEnv Int64 -> Neovim CornelisEnv (Maybe Extmark))
-> Neovim CornelisEnv Int64 -> Neovim CornelisEnv (Maybe Extmark)
forall a b. (a -> b) -> a -> b
$ Buffer
-> Int64
-> Int64
-> Int64
-> Map Text Object
-> Neovim CornelisEnv Int64
forall env.
Buffer
-> Int64 -> Int64 -> Int64 -> Map Text Object -> Neovim env Int64
nvim_buf_set_extmark Buffer
b Int64
ns (LineNumber 'ZeroIndexed -> Int64
forall {e :: Unit}. Index e 'ZeroIndexed -> Int64
from0 LineNumber 'ZeroIndexed
sl) (Index 'Byte 'ZeroIndexed -> Int64
forall {e :: Unit}. Index e 'ZeroIndexed -> Int64
from0 Index 'Byte 'ZeroIndexed
sc)
    (Map Text Object -> Neovim CornelisEnv Int64)
-> Map Text Object -> Neovim CornelisEnv Int64
forall a b. (a -> b) -> a -> b
$ [(Text, Object)] -> Map Text Object
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
    ([(Text, Object)] -> Map Text Object)
-> [(Text, Object)] -> Map Text Object
forall a b. (a -> b) -> a -> b
$ [ ( Text
"end_line"
        , Int64 -> Object
ObjectInt (Int64 -> Object) -> Int64 -> Object
forall a b. (a -> b) -> a -> b
$ LineNumber 'ZeroIndexed -> Int64
forall {e :: Unit}. Index e 'ZeroIndexed -> Int64
from0 LineNumber 'ZeroIndexed
el
        )
      , ( Text
"end_col"
        , Int64 -> Object
ObjectInt (Int64 -> Object) -> Int64 -> Object
forall a b. (a -> b) -> a -> b
$ Index 'Byte 'ZeroIndexed -> Int64
forall {e :: Unit}. Index e 'ZeroIndexed -> Int64
from0 Index 'Byte 'ZeroIndexed
ec
        )
      ] [(Text, Object)] -> [(Text, Object)] -> [(Text, Object)]
forall a. [a] -> [a] -> [a]
++
      (HighlightGroup -> [(Text, Object)])
-> Maybe HighlightGroup -> [(Text, Object)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\HighlightGroup
hl' ->
          [ ( Text
"hl_group"
            , 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
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ HighlightGroup -> String
forall a. Show a => a -> String
show HighlightGroup
hl'
            )
          , ( Text
"priority"
            , Int64 -> Object
ObjectInt (Int64 -> Object) -> Int64 -> Object
forall a b. (a -> b) -> a -> b
$ HighlightGroup -> Int64
priority HighlightGroup
hl'
            )
          ])
          Maybe HighlightGroup
hl


highlightInterval
    :: Buffer
    -> AgdaInterval
    -> HighlightGroup
    -> Neovim CornelisEnv (Maybe Extmark)
highlightInterval :: Buffer
-> AgdaInterval
-> HighlightGroup
-> Neovim CornelisEnv (Maybe Extmark)
highlightInterval Buffer
b AgdaInterval
int HighlightGroup
hl = do
  Interval VimPos
int' <- (AgdaPos -> Neovim CornelisEnv VimPos)
-> AgdaInterval -> Neovim CornelisEnv (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 CornelisEnv VimPos
forall env. Buffer -> AgdaPos -> Neovim env VimPos
vimify Buffer
b) AgdaInterval
int
  Buffer
-> Interval VimPos
-> Maybe HighlightGroup
-> Neovim CornelisEnv (Maybe Extmark)
setHighlight Buffer
b Interval VimPos
int' (Maybe HighlightGroup -> Neovim CornelisEnv (Maybe Extmark))
-> Maybe HighlightGroup -> Neovim CornelisEnv (Maybe Extmark)
forall a b. (a -> b) -> a -> b
$ HighlightGroup -> Maybe HighlightGroup
forall a. a -> Maybe a
Just HighlightGroup
hl


parseExtmark :: Buffer -> Object -> Neovim CornelisEnv (Maybe ExtmarkStuff)
parseExtmark :: Buffer -> Object -> Neovim CornelisEnv (Maybe ExtmarkStuff)
parseExtmark Buffer
b
  (ObjectArray ( (Object -> Maybe Int64
forall a. Num a => Object -> Maybe a
objectToInt -> Just Int64
ext)
               : (forall a. Num a => Object -> Maybe a
objectToInt @Int -> Just (Int -> LineNumber 'ZeroIndexed
forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed -> LineNumber 'ZeroIndexed
start_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
start_col))
               : ObjectMap Map Object Object
details
               : [Object]
_
               )) = MaybeT (Neovim CornelisEnv) ExtmarkStuff
-> Neovim CornelisEnv (Maybe ExtmarkStuff)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (Neovim CornelisEnv) ExtmarkStuff
 -> Neovim CornelisEnv (Maybe ExtmarkStuff))
-> MaybeT (Neovim CornelisEnv) ExtmarkStuff
-> Neovim CornelisEnv (Maybe ExtmarkStuff)
forall a b. (a -> b) -> a -> b
$ do
  Index 'Byte 'ZeroIndexed
end_col <- Maybe (Index 'Byte 'ZeroIndexed)
-> MaybeT (Neovim CornelisEnv) (Index 'Byte 'ZeroIndexed)
forall (m :: * -> *) b. Applicative m => Maybe b -> MaybeT m b
hoistMaybe (Maybe (Index 'Byte 'ZeroIndexed)
 -> MaybeT (Neovim CornelisEnv) (Index 'Byte 'ZeroIndexed))
-> Maybe (Index 'Byte 'ZeroIndexed)
-> MaybeT (Neovim CornelisEnv) (Index 'Byte 'ZeroIndexed)
forall a b. (a -> b) -> a -> b
$ (Int -> Index 'Byte 'ZeroIndexed)
-> Maybe Int -> Maybe (Index 'Byte '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 'Byte 'ZeroIndexed
forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed
            (Maybe Int -> Maybe (Index 'Byte 'ZeroIndexed))
-> (Object -> Maybe Int)
-> Object
-> Maybe (Index 'Byte 'ZeroIndexed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Object -> Maybe a
objectToInt @Int (Object -> Maybe (Index 'Byte 'ZeroIndexed))
-> Maybe Object -> Maybe (Index 'Byte 'ZeroIndexed)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Object -> Map Object Object -> Maybe Object
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (ByteString -> Object
ObjectString ByteString
"end_col") Map Object Object
details
  LineNumber 'ZeroIndexed
end_line <- Maybe (LineNumber 'ZeroIndexed)
-> MaybeT (Neovim CornelisEnv) (LineNumber 'ZeroIndexed)
forall (m :: * -> *) b. Applicative m => Maybe b -> MaybeT m b
hoistMaybe (Maybe (LineNumber 'ZeroIndexed)
 -> MaybeT (Neovim CornelisEnv) (LineNumber 'ZeroIndexed))
-> Maybe (LineNumber 'ZeroIndexed)
-> MaybeT (Neovim CornelisEnv) (LineNumber 'ZeroIndexed)
forall a b. (a -> b) -> a -> b
$ (Int -> LineNumber 'ZeroIndexed)
-> Maybe Int -> Maybe (LineNumber 'ZeroIndexed)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> LineNumber 'ZeroIndexed
forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed
            (Maybe Int -> Maybe (LineNumber 'ZeroIndexed))
-> (Object -> Maybe Int)
-> Object
-> Maybe (LineNumber 'ZeroIndexed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Object -> Maybe a
objectToInt @Int (Object -> Maybe (LineNumber 'ZeroIndexed))
-> Maybe Object -> Maybe (LineNumber 'ZeroIndexed)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Object -> Map Object Object -> Maybe Object
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (ByteString -> Object
ObjectString ByteString
"end_row") Map Object Object
details
  Text
hlgroup <- Maybe Text -> MaybeT (Neovim CornelisEnv) Text
forall (m :: * -> *) b. Applicative m => Maybe b -> MaybeT m b
hoistMaybe (Maybe Text -> MaybeT (Neovim CornelisEnv) Text)
-> Maybe Text -> MaybeT (Neovim CornelisEnv) Text
forall a b. (a -> b) -> a -> b
$ Object -> Maybe Text
objectToText (Object -> Maybe Text) -> Maybe Object -> Maybe Text
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Object -> Map Object Object -> Maybe Object
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (ByteString -> Object
ObjectString ByteString
"hl_group") Map Object Object
details
  AgdaInterval
int <- Neovim CornelisEnv AgdaInterval
-> MaybeT (Neovim CornelisEnv) AgdaInterval
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Neovim CornelisEnv AgdaInterval
 -> MaybeT (Neovim CornelisEnv) AgdaInterval)
-> Neovim CornelisEnv AgdaInterval
-> MaybeT (Neovim CornelisEnv) AgdaInterval
forall a b. (a -> b) -> a -> b
$ (VimPos -> Neovim CornelisEnv AgdaPos)
-> Interval VimPos -> Neovim CornelisEnv AgdaInterval
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 CornelisEnv AgdaPos
forall env. Buffer -> VimPos -> Neovim env AgdaPos
unvimify Buffer
b) (VimPos -> VimPos -> Interval VimPos
forall p. p -> p -> Interval p
Interval (LineNumber 'ZeroIndexed -> Index 'Byte 'ZeroIndexed -> VimPos
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos LineNumber 'ZeroIndexed
start_line Index 'Byte 'ZeroIndexed
start_col) (LineNumber 'ZeroIndexed -> Index 'Byte 'ZeroIndexed -> VimPos
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos LineNumber 'ZeroIndexed
end_line Index 'Byte 'ZeroIndexed
end_col))
  ExtmarkStuff -> MaybeT (Neovim CornelisEnv) ExtmarkStuff
forall a. a -> MaybeT (Neovim CornelisEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExtmarkStuff -> MaybeT (Neovim CornelisEnv) ExtmarkStuff)
-> ExtmarkStuff -> MaybeT (Neovim CornelisEnv) ExtmarkStuff
forall a b. (a -> b) -> a -> b
$ ExtmarkStuff
    { es_mark :: Extmark
es_mark = Int64 -> Extmark
Extmark Int64
ext
    , es_hlgroup :: Text
es_hlgroup = Text
hlgroup
    , es_interval :: AgdaInterval
es_interval = AgdaInterval
int
    }
parseExtmark Buffer
_ Object
_ = Maybe ExtmarkStuff -> Neovim CornelisEnv (Maybe ExtmarkStuff)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ExtmarkStuff
forall a. Maybe a
Nothing

#if __GLASGOW_HASKELL__ <= 904
hoistMaybe :: Applicative m => Maybe a -> MaybeT m a
hoistMaybe = MaybeT . pure
#endif


getExtmarks :: Buffer -> AgdaPos -> Neovim CornelisEnv [ExtmarkStuff]
getExtmarks :: Buffer -> AgdaPos -> Neovim CornelisEnv [ExtmarkStuff]
getExtmarks Buffer
b AgdaPos
p = do
  Int64
ns <- (CornelisEnv -> Int64) -> Neovim CornelisEnv Int64
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CornelisEnv -> Int64
ce_namespace
  VimPos
vp <- Buffer -> AgdaPos -> Neovim CornelisEnv VimPos
forall env. Buffer -> AgdaPos -> Neovim env VimPos
vimify Buffer
b AgdaPos
p
  let -- i = 0 for beginning of line, i = -1 for end of line
      pos :: Int64 -> Object
pos Int64
i = [Object] -> Object
ObjectArray [ Int64 -> Object
ObjectInt (Int64 -> Object) -> Int64 -> Object
forall a b. (a -> b) -> a -> b
$ LineNumber 'ZeroIndexed -> Int64
forall a (e :: Unit). Num a => Index e 'ZeroIndexed -> a
fromZeroIndexed (VimPos -> LineNumber 'ZeroIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index 'Line i
p_line VimPos
vp)
                          , Int64 -> Object
ObjectInt Int64
i
                          ]
  Vector Object
res <- Buffer
-> Int64
-> Object
-> Object
-> Map Text Object
-> Neovim CornelisEnv (Vector Object)
forall env.
Buffer
-> Int64
-> Object
-> Object
-> Map Text Object
-> Neovim env (Vector Object)
nvim_buf_get_extmarks Buffer
b Int64
ns (Int64 -> Object
pos Int64
0) (Int64 -> Object
pos (-Int64
1)) (Map Text Object -> Neovim CornelisEnv (Vector Object))
-> Map Text Object -> Neovim CornelisEnv (Vector Object)
forall a b. (a -> b) -> a -> b
$ Text -> Object -> Map Text Object
forall k a. k -> a -> Map k a
M.singleton Text
"details" (Object -> Map Text Object) -> Object -> Map Text Object
forall a b. (a -> b) -> a -> b
$ Bool -> Object
ObjectBool Bool
True
  [ExtmarkStuff]
marks <- ([Maybe ExtmarkStuff] -> [ExtmarkStuff])
-> Neovim CornelisEnv [Maybe ExtmarkStuff]
-> Neovim CornelisEnv [ExtmarkStuff]
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe ExtmarkStuff] -> [ExtmarkStuff]
forall a. [Maybe a] -> [a]
catMaybes (Neovim CornelisEnv [Maybe ExtmarkStuff]
 -> Neovim CornelisEnv [ExtmarkStuff])
-> Neovim CornelisEnv [Maybe ExtmarkStuff]
-> Neovim CornelisEnv [ExtmarkStuff]
forall a b. (a -> b) -> a -> b
$ (Object -> Neovim CornelisEnv (Maybe ExtmarkStuff))
-> [Object] -> Neovim CornelisEnv [Maybe ExtmarkStuff]
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) -> [a] -> f [b]
traverse (Buffer -> Object -> Neovim CornelisEnv (Maybe ExtmarkStuff)
parseExtmark Buffer
b) ([Object] -> Neovim CornelisEnv [Maybe ExtmarkStuff])
-> [Object] -> Neovim CornelisEnv [Maybe ExtmarkStuff]
forall a b. (a -> b) -> a -> b
$ Vector Object -> [Object]
forall a. Vector a -> [a]
V.toList Vector Object
res

  [ExtmarkStuff] -> Neovim CornelisEnv [ExtmarkStuff]
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ExtmarkStuff] -> Neovim CornelisEnv [ExtmarkStuff])
-> [ExtmarkStuff] -> Neovim CornelisEnv [ExtmarkStuff]
forall a b. (a -> b) -> a -> b
$ [ExtmarkStuff]
marks [ExtmarkStuff]
-> (ExtmarkStuff -> [ExtmarkStuff]) -> [ExtmarkStuff]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ExtmarkStuff
es ->
    case AgdaInterval -> AgdaPos -> Bool
forall p. Ord p => Interval p -> p -> Bool
containsPoint (ExtmarkStuff -> AgdaInterval
es_interval ExtmarkStuff
es) AgdaPos
p of
      Bool
False -> [ExtmarkStuff]
forall a. Monoid a => a
mempty
      Bool
True -> [ExtmarkStuff
es]