-- | 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)
               ]