{-# LANGUAGE CPP #-}
module Agda.Interaction.Highlighting.Emacs
( lispifyHighlightingInfo
, lispifyTokenBased
) where
import Agda.Interaction.Highlighting.Common
import Agda.Interaction.Highlighting.Precise
import Agda.Interaction.Highlighting.Range (Range(..))
import Agda.Interaction.EmacsCommand
import Agda.Interaction.Response
import Agda.TypeChecking.Monad (HighlightingMethod(..), ModuleToSource)
import Agda.Utils.FileName (filePath)
import Agda.Utils.IO.TempFile (writeToTempFile)
import Agda.Utils.String (quote)
import qualified Data.List as List
import qualified Data.Map as Map
import Data.Maybe
#include "undefined.h"
import Agda.Utils.Impossible
showAspects
:: ModuleToSource
-> (Range, Aspects) -> Lisp String
showAspects modFile (r, m) = L $
(map (A . show) [from r, to r])
++
[L $ map A $ toAtoms m]
++
dropNils (
[lispifyTokenBased (tokenBased m)]
++
[A $ maybe "nil" quote $ note m]
++
(maybeToList $ fmap defSite $ definitionSite m))
where
defSite (DefinitionSite m p _ _) =
Cons (A $ quote $ filePath f) (A $ show p)
where f = Map.findWithDefault __IMPOSSIBLE__ m modFile
dropNils = List.dropWhileEnd (== A "nil")
lispifyTokenBased :: TokenBased -> Lisp String
lispifyTokenBased TokenBased = A "t"
lispifyTokenBased NotOnlyTokenBased = A "nil"
lispifyHighlightingInfo
:: HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> IO (Lisp String)
lispifyHighlightingInfo h remove method modFile =
case chooseHighlightingMethod h method of
Direct -> direct
Indirect -> indirect
where
info :: [Lisp String]
info = (case remove of
RemoveHighlighting -> A "remove"
KeepHighlighting -> A "nil") :
map (showAspects modFile) (ranges h)
direct :: IO (Lisp String)
direct = return $ L (A "agda2-highlight-add-annotations" :
map Q info)
indirect :: IO (Lisp String)
indirect = do
filepath <- writeToTempFile (show $ L info)
return $ L [ A "agda2-highlight-load-and-delete-action"
, A (quote filepath)
]