-- | 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. module Cornelis.Diff ( resetDiff , translateInterval , recordUpdate , Replace(..) , Colline(..) , Vallee(..) ) where import Data.IORef (atomicModifyIORef') import qualified Data.Map as Map import Data.Tuple (swap) import DiffLoc (Replace(..), Colline(..), Vallee(..)) import qualified DiffLoc as D import Neovim import Cornelis.Offsets import Cornelis.Types -- | A general function for modifying Diffs, shared between the three functions below. modifyDiff :: BufferNum -> (Diff0 -> (Diff0, a)) -> Neovim CornelisEnv a modifyDiff buf f = do csRef <- asks ce_state liftIO $ atomicModifyIORef' csRef $ \cs -> let (a, ds') = Map.alterF (fmap Just . swap . alter) buf (cs_diff cs) in (cs { cs_diff = ds' }, a) where alter Nothing = f D.emptyDiff alter (Just d) = f d -- These three functions are essentially monadic wrappers, using 'modifyDiff', -- around the corresponding diff-loc functions: -- -- @ -- 'D.emptyDiff' :: Diff0 -- 'D.addDiff' :: D.Replace DPos -> Diff0 -> Diff0 -- 'D.mapDiff' :: Diff0 -> D.Interval DPos -> Maybe (D.Interval DPos) -- @ -- -- This relies on instances of 'D.Amor' and 'D.Origin' implemented in 'Cornelis.Offsets'. -- | Reset the diff to an empty diff. resetDiff :: BufferNum -> Neovim CornelisEnv () resetDiff buf = modifyDiff buf $ const (D.emptyDiff, ()) -- | 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. recordUpdate :: BufferNum -> D.Replace DPos -> Neovim CornelisEnv () recordUpdate buf r = modifyDiff buf $ \d -> (D.addDiff r d, ()) -- | 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. translateInterval :: BufferNum -> Interval VimPos -> Neovim CornelisEnv (Maybe (Interval VimPos)) translateInterval buf sp = modifyDiff buf $ \d -> (d, translate d) where translate :: Diff0 -> Maybe (Interval VimPos) translate d = fmap toInterval . D.mapDiff d =<< fromInterval sp -- | Convert a Cornelis interval (pair of positions) to a diff-loc interval -- (start position and a vector towards the end position). This is Nothing -- if the end precedes the start. fromInterval :: Interval VimPos -> Maybe (D.Interval DPos) fromInterval (Interval p1 p2) = (q1 D.:..) <$> (q2 D..-.? q1) where q1 = fromVimPos p1 q2 = fromVimPos p2 -- | Inverse of 'fromInterval'. toInterval :: D.Interval DPos -> Interval VimPos toInterval (q D.:.. v) = Interval (toVimPos q) (toVimPos (q D..+ v)) -- | Convert from Cornelis positions to diff-loc positions. fromVimPos :: VimPos -> DPos fromVimPos (Pos l c) = Colline l c toVimPos :: DPos -> VimPos toVimPos (Colline l c) = Pos l c