{-# OPTIONS_GHC -Wunused-imports #-}

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

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

import Prelude hiding (null)

import qualified Data.List as List
import Data.Maybe

import Agda.Syntax.Common.Pretty (prettyShow)

import Agda.Interaction.Highlighting.Common
import Agda.Interaction.Highlighting.Precise
import Agda.Utils.Range (Range(..))
import Agda.Interaction.Emacs.Lisp
import Agda.Interaction.Response

import Agda.TypeChecking.Monad (HighlightingMethod(..), ModuleToSource, topLevelModuleFilePath)

import Agda.Utils.CallStack    (HasCallStack)
import Agda.Utils.FileName     (AbsolutePath, filePath)
import Agda.Utils.IO.TempFile  (writeToTempFile)
import Agda.Utils.Null
import Agda.Utils.String       (quote)


-- | 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 [Char]
showAspects ModuleToSource
modFile (Range
r, Aspects
m) = [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$
    ((Int -> Lisp [Char]) -> [Int] -> [Lisp [Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char]) -> (Int -> [Char]) -> Int -> Lisp [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show) [Range -> Int
from Range
r, Range -> Int
to Range
r])
      [Lisp [Char]] -> [Lisp [Char]] -> [Lisp [Char]]
forall a. [a] -> [a] -> [a]
++
    [[Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ ([Char] -> Lisp [Char]) -> [[Char]] -> [Lisp [Char]]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([[Char]] -> [Lisp [Char]]) -> [[Char]] -> [Lisp [Char]]
forall a b. (a -> b) -> a -> b
$ Aspects -> [[Char]]
toAtoms Aspects
m]
      [Lisp [Char]] -> [Lisp [Char]] -> [Lisp [Char]]
forall a. [a] -> [a] -> [a]
++
    [Lisp [Char]] -> [Lisp [Char]]
dropNils (
      [TokenBased -> Lisp [Char]
lispifyTokenBased (Aspects -> TokenBased
tokenBased Aspects
m)]
        [Lisp [Char]] -> [Lisp [Char]] -> [Lisp [Char]]
forall a. [a] -> [a] -> [a]
++
      [[Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> ([Char] -> [Char]) -> [Char]
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (Aspects -> [Char]
note Aspects
m) [Char]
"nil" [Char] -> [Char]
quote]
        [Lisp [Char]] -> [Lisp [Char]] -> [Lisp [Char]]
forall a. [a] -> [a] -> [a]
++
      Maybe (Lisp [Char]) -> [Lisp [Char]]
forall a. Maybe a -> [a]
maybeToList (DefinitionSite -> Lisp [Char]
defSite (DefinitionSite -> Lisp [Char])
-> Maybe DefinitionSite -> Maybe (Lisp [Char])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Aspects -> Maybe DefinitionSite
definitionSite Aspects
m))
  where
  defSite :: DefinitionSite -> Lisp [Char]
defSite (DefinitionSite TopLevelModuleName' Range
m Int
p Bool
_ Maybe [Char]
_) =
    Lisp [Char] -> Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a -> Lisp a
Cons ([Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
quote ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath AbsolutePath
HasCallStack => AbsolutePath
f) ([Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
p)
    where
      f :: HasCallStack => AbsolutePath
      f :: HasCallStack => AbsolutePath
f = HasCallStack =>
ModuleToSource -> TopLevelModuleName' Range -> AbsolutePath
ModuleToSource -> TopLevelModuleName' Range -> AbsolutePath
topLevelModuleFilePath ModuleToSource
modFile TopLevelModuleName' Range
m  -- partial function, so use CallStack!

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

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

lispifyTokenBased :: TokenBased -> Lisp String
lispifyTokenBased :: TokenBased -> Lisp [Char]
lispifyTokenBased TokenBased
TokenBased        = [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"t"
lispifyTokenBased TokenBased
NotOnlyTokenBased = [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"nil"

-- | Run 'showAspects' on a whole 'RangeMap'.
lispifyHighlightingInfo_ ::
     ModuleToSource
       -- ^ Must contain a mapping for every definition site's module.
  -> HighlightingInfo
  -> [Lisp String]
lispifyHighlightingInfo_ :: ModuleToSource -> RangeMap Aspects -> [Lisp [Char]]
lispifyHighlightingInfo_ ModuleToSource
m2s = ((Range, Aspects) -> Lisp [Char])
-> [(Range, Aspects)] -> [Lisp [Char]]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleToSource -> (Range, Aspects) -> Lisp [Char]
showAspects ModuleToSource
m2s) ([(Range, Aspects)] -> [Lisp [Char]])
-> (RangeMap Aspects -> [(Range, Aspects)])
-> RangeMap Aspects
-> [Lisp [Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeMap Aspects -> [(Range, Aspects)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList

-- | 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 :: RangeMap Aspects
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> IO (Lisp [Char])
lispifyHighlightingInfo RangeMap Aspects
h RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile =
  case RangeMap Aspects -> HighlightingMethod -> HighlightingMethod
chooseHighlightingMethod RangeMap Aspects
h HighlightingMethod
method of
    HighlightingMethod
Direct   -> IO (Lisp [Char])
direct
    HighlightingMethod
Indirect -> IO (Lisp [Char])
indirect
  where
  info :: [Lisp String]
  info :: [Lisp [Char]]
info =
    [Char] -> Lisp [Char]
forall a. a -> Lisp a
A (case RemoveTokenBasedHighlighting
remove of
        RemoveTokenBasedHighlighting
RemoveHighlighting -> [Char]
"remove"
        RemoveTokenBasedHighlighting
KeepHighlighting   -> [Char]
"nil") Lisp [Char] -> [Lisp [Char]] -> [Lisp [Char]]
forall a. a -> [a] -> [a]
:
    ModuleToSource -> RangeMap Aspects -> [Lisp [Char]]
lispifyHighlightingInfo_ ModuleToSource
modFile RangeMap Aspects
h

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

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