{-# 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 b = do buf_lines <- nvim_buf_get_lines b 0 (-1) True pure $ getLineIntervals buf_lines updateLineIntervals :: Buffer -> Neovim CornelisEnv () updateLineIntervals b = do li <- lineIntervalsForBuffer b modifyBufferStuff b $ #bs_code_map .~ li highlightBuffer :: Buffer -> [Highlight] -> Neovim CornelisEnv (M.Map AgdaInterval Extmark) highlightBuffer b hs = withBufferStuff b $ \bs -> do let li = bs_code_map bs (holes, exts) <- fmap unzip $ for hs $ \hl -> do (hole, mext) <- addHighlight b li hl pure (hole, (hl, mext)) let zs = catMaybes $ do (hl, mext) <- exts pure $ do ext <- mext ds <- hl_definitionSite hl pure (ext, ds) modifyBufferStuff b $ #bs_goto_sites <>~ M.fromList zs pure $ mconcat holes getLineIntervals :: Vector Text -> LineIntervals getLineIntervals = LineIntervals . go (toOneIndexed @Int 1) (toZeroIndexed @Int 0) where go :: AgdaIndex -> LineNumber 'ZeroIndexed -> Vector Text -> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text) go pos line v | Just (t, ss) <- V.uncons v = let len = T.length t pos' = pos .+ Offset len in IM.insert (IM.Interval pos pos') (line, t) $ go (incIndex pos') (incIndex line) ss | otherwise = mempty lookupPoint :: LineIntervals -> AgdaIndex -> Maybe VimPos lookupPoint (LineIntervals im) i = do (IM.Interval lineStart _, (line, s)) <- listToMaybe $ IM.search i im let col = toBytes s (toZeroIndexed @Int 0 .+ (i .-. lineStart)) pure (Pos line col) ------------------------------------------------------------------------------ -- | Returns any holes it tried to highlight on the left addHighlight :: Buffer -> LineIntervals -> Highlight -> Neovim CornelisEnv (M.Map AgdaInterval Extmark, Maybe Extmark) addHighlight b lis hl = do case Interval <$> lookupPoint lis (hl_start hl) <*> lookupPoint lis (hl_end hl) of Just int@(Interval start end) -> do ext <- setHighlight b int $ parseHighlightGroup hl fmap (, ext) $ case isHole hl of False -> pure mempty True -> do let vint = Interval start end aint <- traverse (unvimify b) vint pure $ maybe mempty (M.singleton aint) ext Nothing -> pure (mempty, 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 = listToMaybe . mapMaybe atomToHlGroup . hl_atoms isHole :: Highlight -> Bool isHole = elem "hole" . hl_atoms setHighlight :: Buffer -> Interval VimPos -> Maybe HighlightGroup -> Neovim CornelisEnv (Maybe Extmark) setHighlight b i hl = do bn <- buffer_get_number b mi' <- translateInterval bn i case mi' of Just i' -> setHighlight' b i' hl Nothing -> pure Nothing setHighlight' :: Buffer -> Interval VimPos -> Maybe HighlightGroup -> Neovim CornelisEnv (Maybe Extmark) setHighlight' b (Interval (Pos sl sc) (Pos el ec)) hl = do ns <- asks ce_namespace let from0 = fromZeroIndexed flip catchNeovimException (const (pure Nothing)) $ fmap (Just . coerce) $ nvim_buf_set_extmark b ns (from0 sl) (from0 sc) $ M.fromList $ [ ( "end_line" , ObjectInt $ from0 el ) , ( "end_col" , ObjectInt $ from0 ec ) ] ++ concatMap (\hl' -> [ ( "hl_group" , ObjectString $ encodeUtf8 $ T.pack $ show hl' ) , ( "priority" , ObjectInt $ priority hl' ) ]) hl highlightInterval :: Buffer -> AgdaInterval -> HighlightGroup -> Neovim CornelisEnv (Maybe Extmark) highlightInterval b int hl = do int' <- traverse (vimify b) int setHighlight b int' $ Just hl parseExtmark :: Buffer -> Object -> Neovim CornelisEnv (Maybe ExtmarkStuff) parseExtmark b (ObjectArray ( (objectToInt -> Just ext) : (objectToInt @Int -> Just (toZeroIndexed -> start_line)) : (objectToInt @Int -> Just (toZeroIndexed -> start_col)) : ObjectMap details : _ )) = runMaybeT $ do end_col <- hoistMaybe $ fmap toZeroIndexed . objectToInt @Int =<< M.lookup (ObjectString "end_col") details end_line <- hoistMaybe $ fmap toZeroIndexed . objectToInt @Int =<< M.lookup (ObjectString "end_row") details hlgroup <- hoistMaybe $ objectToText =<< M.lookup (ObjectString "hl_group") details int <- lift $ traverse (unvimify b) (Interval (Pos start_line start_col) (Pos end_line end_col)) pure $ ExtmarkStuff { es_mark = Extmark ext , es_hlgroup = hlgroup , es_interval = int } parseExtmark _ _ = pure Nothing #if __GLASGOW_HASKELL__ <= 904 hoistMaybe :: Applicative m => Maybe a -> MaybeT m a hoistMaybe = MaybeT . pure #endif getExtmarks :: Buffer -> AgdaPos -> Neovim CornelisEnv [ExtmarkStuff] getExtmarks b p = do ns <- asks ce_namespace vp <- vimify b p let -- i = 0 for beginning of line, i = -1 for end of line pos i = ObjectArray [ ObjectInt $ fromZeroIndexed (p_line vp) , ObjectInt i ] res <- nvim_buf_get_extmarks b ns (pos 0) (pos (-1)) $ M.singleton "details" $ ObjectBool True marks <- fmap catMaybes $ traverse (parseExtmark b) $ V.toList res pure $ marks >>= \es -> case containsPoint (es_interval es) p of False -> mempty True -> [es]