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

    module Agda.Interaction.Highlighting.Emacs
      ( lispifyHighlightingInfo
      , lispifyTokenBased
      ) where

    import Prelude hiding (null)

    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.Pretty (prettyShow)
    import Agda.Utils.String (quote)

    import qualified Data.List as List
    import qualified Data.Map as Map
    import Data.Maybe

    import Agda.Utils.Null
    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 :: ModuleToSource -> (Range, Aspects) -> Lisp String
    showAspects ModuleToSource
    modFile (Range
    r, Aspects
    m) = [Lisp String] -> Lisp String
    forall a. [Lisp a] -> Lisp a
    L ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
    forall a b. (a -> b) -> a -> b
    $
        ((Int -> Lisp String) -> [Int] -> [Lisp String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String -> Lisp String
    forall a. a -> Lisp a
    A (String -> Lisp String) -> (Int -> String) -> Int -> Lisp String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> String
    forall a. Show a => a -> String
    show) [Range -> Int
    from Range
    r, Range -> Int
    to Range
    r])
          [Lisp String] -> [Lisp String] -> [Lisp String]
    forall a. [a] -> [a] -> [a]
    ++
        [[Lisp String] -> Lisp String
    forall a. [Lisp a] -> Lisp a
    L ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
    forall a b. (a -> b) -> a -> b
    $ (String -> Lisp String) -> [String] -> [Lisp String]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Lisp String
    forall a. a -> Lisp a
    A ([String] -> [Lisp String]) -> [String] -> [Lisp String]
    forall a b. (a -> b) -> a -> b
    $ Aspects -> [String]
    toAtoms Aspects
    m]
          [Lisp String] -> [Lisp String] -> [Lisp String]
    forall a. [a] -> [a] -> [a]
    ++
        [Lisp String] -> [Lisp String]
    dropNils (
          [TokenBased -> Lisp String
    lispifyTokenBased (Aspects -> TokenBased
    tokenBased Aspects
    m)]
            [Lisp String] -> [Lisp String] -> [Lisp String]
    forall a. [a] -> [a] -> [a]
    ++
          [String -> Lisp String
    forall a. a -> Lisp a
    A (String -> Lisp String) -> String -> Lisp String
    forall a b. (a -> b) -> a -> b
    $ String -> String -> (String -> String) -> String
    forall a b. Null a => a -> b -> (a -> b) -> b
    ifNull (Aspects -> String
    note Aspects
    m) String
    "nil" String -> String
    quote]
            [Lisp String] -> [Lisp String] -> [Lisp String]
    forall a. [a] -> [a] -> [a]
    ++
          Maybe (Lisp String) -> [Lisp String]
    forall a. Maybe a -> [a]
    maybeToList (DefinitionSite -> Lisp String
    defSite (DefinitionSite -> Lisp String)
    -> Maybe DefinitionSite -> Maybe (Lisp String)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Aspects -> Maybe DefinitionSite
    definitionSite Aspects
    m))
      where
      defSite :: DefinitionSite -> Lisp String
    defSite (DefinitionSite TopLevelModuleName
    m Int
    p Bool
    _ Maybe String
    _) =
        Lisp String -> Lisp String -> Lisp String
    forall a. Lisp a -> Lisp a -> Lisp a
    Cons (String -> Lisp String
    forall a. a -> Lisp a
    A (String -> Lisp String) -> String -> Lisp String
    forall a b. (a -> b) -> a -> b
    $ String -> String
    quote (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> String
    filePath AbsolutePath
    f) (String -> Lisp String
    forall a. a -> Lisp a
    A (String -> Lisp String) -> String -> Lisp String
    forall a b. (a -> b) -> a -> b
    $ Int -> String
    forall a. Show a => a -> String
    show Int
    p)
        where f :: AbsolutePath
    f = AbsolutePath
    -> TopLevelModuleName -> ModuleToSource -> AbsolutePath
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault AbsolutePath
    forall a. HasCallStack => a
    __IMPOSSIBLE__ TopLevelModuleName
    m ModuleToSource
    modFile

      dropNils :: [Lisp String] -> [Lisp String]
    dropNils = (Lisp String -> Bool) -> [Lisp String] -> [Lisp String]
    forall a. (a -> Bool) -> [a] -> [a]
    List.dropWhileEnd (Lisp String -> Lisp String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String -> Lisp String
    forall a. a -> Lisp a
    A String
    "nil")

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

    lispifyTokenBased :: TokenBased -> Lisp String
    lispifyTokenBased :: TokenBased -> Lisp String
    lispifyTokenBased TokenBased
    TokenBased        = String -> Lisp String
    forall a. a -> Lisp a
    A String
    "t"
    lispifyTokenBased TokenBased
    NotOnlyTokenBased = String -> Lisp String
    forall a. a -> Lisp a
    A String
    "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 :: HighlightingInfo
    -> RemoveTokenBasedHighlighting
    -> HighlightingMethod
    -> ModuleToSource
    -> IO (Lisp String)
    lispifyHighlightingInfo HighlightingInfo
    h RemoveTokenBasedHighlighting
    remove HighlightingMethod
    method ModuleToSource
    modFile =
      case HighlightingInfo -> HighlightingMethod -> HighlightingMethod
    chooseHighlightingMethod HighlightingInfo
    h HighlightingMethod
    method of
        HighlightingMethod
    Direct   -> IO (Lisp String)
    direct
        HighlightingMethod
    Indirect -> IO (Lisp String)
    indirect
      where
      info :: [Lisp String]
      info :: [Lisp String]
    info = (case RemoveTokenBasedHighlighting
    remove of
                    RemoveTokenBasedHighlighting
    RemoveHighlighting -> String -> Lisp String
    forall a. a -> Lisp a
    A String
    "remove"
                    RemoveTokenBasedHighlighting
    KeepHighlighting   -> String -> Lisp String
    forall a. a -> Lisp a
    A String
    "nil") Lisp String -> [Lisp String] -> [Lisp String]
    forall a. a -> [a] -> [a]
    :
                 ((Range, Aspects) -> Lisp String)
    -> [(Range, Aspects)] -> [Lisp String]
    forall a b. (a -> b) -> [a] -> [b]
    map (ModuleToSource -> (Range, Aspects) -> Lisp String
    showAspects ModuleToSource
    modFile) (HighlightingInfo -> [(Range, Aspects)]
    forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
    toList HighlightingInfo
    h)

      direct :: IO (Lisp String)
      direct :: IO (Lisp String)
    direct = Lisp String -> IO (Lisp String)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Lisp String -> IO (Lisp String))
    -> Lisp String -> IO (Lisp String)
    forall a b. (a -> b) -> a -> b
    $ [Lisp String] -> Lisp String
    forall a. [Lisp a] -> Lisp a
    L (String -> Lisp String
    forall a. a -> Lisp a
    A String
    "agda2-highlight-add-annotations" Lisp String -> [Lisp String] -> [Lisp String]
    forall a. a -> [a] -> [a]
    :
                             (Lisp String -> Lisp String) -> [Lisp String] -> [Lisp String]
    forall a b. (a -> b) -> [a] -> [b]
    map Lisp String -> Lisp String
    forall a. Lisp a -> Lisp a
    Q [Lisp String]
    info)

      indirect :: IO (Lisp String)
      indirect :: IO (Lisp String)
    indirect = do
        String
    filepath <- String -> IO String
    writeToTempFile (Lisp String -> String
    forall a. Pretty a => a -> String
    prettyShow (Lisp String -> String) -> Lisp String -> String
    forall a b. (a -> b) -> a -> b
    $ [Lisp String] -> Lisp String
    forall a. [Lisp a] -> Lisp a
    L [Lisp String]
    info)
        Lisp String -> IO (Lisp String)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Lisp String -> IO (Lisp String))
    -> Lisp String -> IO (Lisp String)
    forall a b. (a -> b) -> a -> b
    $ [Lisp String] -> Lisp String
    forall a. [Lisp a] -> Lisp a
    L [ String -> Lisp String
    forall a. a -> Lisp a
    A String
    "agda2-highlight-load-and-delete-action"
                   , String -> Lisp String
    forall a. a -> Lisp a
    A (String -> String
    quote String
    filepath)
                   ]