{-# OPTIONS_GHC -Wunused-imports #-}
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.Syntax.Common.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
showAspects
:: ModuleToSource
-> (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' Range
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' Range -> ModuleToSource -> AbsolutePath
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault AbsolutePath
forall a. HasCallStack => a
__IMPOSSIBLE__ TopLevelModuleName' Range
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")
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"
lispifyHighlightingInfo
:: HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> 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 a. a -> IO a
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
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)
return $ L [ A "agda2-highlight-load-and-delete-action"
, A (quote filepath)
]