{-# LANGUAGE CPP #-}
module Agda.Interaction.Highlighting.Emacs
( lispifyHighlightingInfo
, lispifyTokenBased
) where
import Agda.Interaction.Highlighting.Precise
import Agda.Interaction.Highlighting.Range
import Agda.Interaction.EmacsCommand
import Agda.Interaction.Response
import Agda.Syntax.Common
import Agda.TypeChecking.Monad
(TCM, envHighlightingMethod, HighlightingMethod(..), ModuleToSource)
import Agda.Utils.FileName
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.String
import qualified Control.Exception as E
import Control.Monad.Reader
import Data.Char
import qualified Data.Map as Map
import Data.Maybe
import Data.Monoid
import qualified System.Directory as D
import qualified System.IO as IO
#include "undefined.h"
import Agda.Utils.Impossible
toAtoms :: Aspects -> [String]
toAtoms m = map toAtom (otherAspects m) ++ toAtoms' (aspect m)
where
toAtom :: Show a => a -> String
toAtom = map toLower . show
kindToAtom (Constructor Inductive) = "inductiveconstructor"
kindToAtom (Constructor CoInductive) = "coinductiveconstructor"
kindToAtom k = toAtom k
toAtoms' Nothing = []
toAtoms' (Just (Name mKind op)) =
map kindToAtom (maybeToList mKind) ++ opAtom
where opAtom | op = ["operator"]
| otherwise = []
toAtoms' (Just a) = [toAtom a]
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 =
reverse .
dropWhile (== A "nil") .
reverse
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 = do
case ranges h of
_ | method == Direct -> direct
((_, mi) : _) | otherAspects mi == [TypeChecks] ||
mi == mempty -> direct
_ -> indirect
where
info = (case remove of
RemoveHighlighting -> A "remove"
KeepHighlighting -> A "nil") :
map (showAspects modFile) (ranges h)
direct = return $ L (A "agda2-highlight-add-annotations" :
map Q info)
indirect = do
dir <- D.getTemporaryDirectory
f <- E.bracket (IO.openTempFile dir "agda2-mode")
(IO.hClose . snd) $ \ (f, h) -> do
UTF8.hPutStr h (show $ L info)
return f
return $ L [ A "agda2-highlight-load-and-delete-action"
, A (quote f)
]