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

  dropNils :: [Lisp String] -> [Lisp String]
dropNils = forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd (forall a. Eq a => a -> a -> Bool
== 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        = forall a. a -> Lisp a
A String
"t"
lispifyTokenBased TokenBased
NotOnlyTokenBased = 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 -> forall a. a -> Lisp a
A String
"remove"
                RemoveTokenBasedHighlighting
KeepHighlighting   -> forall a. a -> Lisp a
A String
"nil") forall a. a -> [a] -> [a]
:
             forall a b. (a -> b) -> [a] -> [b]
map (ModuleToSource -> (Range, Aspects) -> Lisp String
showAspects ModuleToSource
modFile) (forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList HighlightingInfo
h)

  direct :: IO (Lisp String)
  direct :: IO (Lisp String)
direct = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Lisp a] -> Lisp a
L (forall a. a -> Lisp a
A String
"agda2-highlight-add-annotations" forall a. a -> [a] -> [a]
:
                         forall a b. (a -> b) -> [a] -> [b]
map 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 (forall a. Pretty a => a -> String
prettyShow forall a b. (a -> b) -> a -> b
$ forall a. [Lisp a] -> Lisp a
L [Lisp String]
info)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Lisp a] -> Lisp a
L [ forall a. a -> Lisp a
A String
"agda2-highlight-load-and-delete-action"
               , forall a. a -> Lisp a
A (String -> String
quote String
filepath)
               ]