    {-# LANGUAGE CPP #-}

    -- | Functions which give precise syntax highlighting info to Emacs.

    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

    ------------------------------------------------------------------------
    -- Read/show functions

    -- | Shows meta information in such a way that it can easily be read
    -- by Emacs.

    showAspects
      :: ModuleToSource
         -- ^ Must contain a mapping for the definition site's module, if any.
      -> (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")

    -- | Formats the 'TokenBased' tag for the Emacs backend. No quotes are
    -- added.

    lispifyTokenBased :: TokenBased -> Lisp String
    lispifyTokenBased TokenBased        = A "t"
    lispifyTokenBased NotOnlyTokenBased = A "nil"

    -- | Turns syntax highlighting information into a list of
    -- S-expressions.

    -- TODO: The "go-to-definition" targets can contain long strings
    -- (absolute paths to files). At least one of these strings (the path
    -- to the current module) can occur many times. Perhaps it would be a
    -- good idea to use a more compact format.

    lispifyHighlightingInfo
      :: HighlightingInfo
      -> RemoveTokenBasedHighlighting
      -> HighlightingMethod
      -> ModuleToSource
         -- ^ Must contain a mapping for every definition site's module.
      -> 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)
                   ]