------------------------------------------------------------------------
-- | Code for instructing Emacs to do things
------------------------------------------------------------------------

module Agda.Interaction.EmacsCommand
  ( displayInfo
  , clearRunningInfo
  , displayRunningInfo
  , displayVerboseInfo
  ) where

import Prelude hiding (null)

import Data.Bifunctor (second)
import Data.Text qualified as Text

import Agda.Syntax.Common.Pretty           (DocTree)

import Agda.Interaction.Emacs.Lisp
import Agda.Interaction.Highlighting.Emacs (HighlightingInfo, lispifyHighlightingInfo_)

import Agda.TypeChecking.Monad.Base.Types  (ModuleToSource)

import Agda.Utils.Null
import Agda.Utils.String                   (quote)
import Agda.Utils.DocTree                  (treeToTextNoAnn, treeToTextWithAnn)

-- | @displayInfo header content append m@ displays @content@
-- with header @header@ in some suitable way in the Agda information buffer.
-- If @append@ is @True@, then the content is appended to previous content
-- (if any), otherwise any previous content is deleted.
-- If @m@ is @Just 'ModuleToSource'@ then @content@ is rendered with annotations,
-- otherwise annotations in @content@ are discarded and just the text is displayed.

displayInfo :: String -> DocTree -> Bool -> Maybe ModuleToSource -> Lisp String
displayInfo :: [Char]
-> DocTree Aspects -> Bool -> Maybe ModuleToSource -> Lisp [Char]
displayInfo [Char]
header DocTree Aspects
content Bool
append Maybe ModuleToSource
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
$ [[Lisp [Char]]] -> [Lisp [Char]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-info-action"
    , [Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> [Char]
quote [Char]
header)
    , [Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> [Char]
quote ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Text -> [Char]
Text.unpack Text
t)
    , [Char] -> Lisp [Char]
forall a. a -> Lisp a
A (if Bool
append then [Char]
"t" else [Char]
"nil")
    ]
  , (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]]
ann
  ]
  where
    (Text
t, [Lisp [Char]]
ann) = DocTree Aspects -> Maybe ModuleToSource -> (Text, [Lisp [Char]])
processAnnotations DocTree Aspects
content Maybe ModuleToSource
m

------------------------------------------------------------------------
-- Running info

-- | Header to display in the Agda information buffer for "running info".

runningInfoHeader :: String
runningInfoHeader :: [Char]
runningInfoHeader = [Char]
"*Type-checking*"

-- | Clear the running info buffer.

clearRunningInfo :: Lisp String
clearRunningInfo :: Lisp [Char]
clearRunningInfo = [Char]
-> DocTree Aspects -> Bool -> Maybe ModuleToSource -> Lisp [Char]
displayInfo [Char]
runningInfoHeader DocTree Aspects
forall a. Null a => a
empty Bool
False Maybe ModuleToSource
forall a. Maybe a
Nothing

-- | Display running information about what the type-checker is up to.

displayRunningInfo :: DocTree -> Maybe ModuleToSource -> Lisp String
displayRunningInfo :: DocTree Aspects -> Maybe ModuleToSource -> Lisp [Char]
displayRunningInfo DocTree Aspects
t = [Char]
-> DocTree Aspects -> Bool -> Maybe ModuleToSource -> Lisp [Char]
displayInfo [Char]
runningInfoHeader DocTree Aspects
t Bool
True

displayVerboseInfo :: DocTree -> Maybe ModuleToSource -> Lisp String
displayVerboseInfo :: DocTree Aspects -> Maybe ModuleToSource -> Lisp [Char]
displayVerboseInfo DocTree Aspects
t Maybe ModuleToSource
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
$ [[Lisp [Char]]] -> [Lisp [Char]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-verbose"
    , [Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> [Char]
quote ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Text -> [Char]
Text.unpack Text
tx)]
  , (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]]
anns]
  where
    (Text
tx, [Lisp [Char]]
anns) = DocTree Aspects -> Maybe ModuleToSource -> (Text, [Lisp [Char]])
processAnnotations DocTree Aspects
t Maybe ModuleToSource
m

processAnnotations :: DocTree -> Maybe ModuleToSource -> (Text.Text, [Lisp String])
processAnnotations :: DocTree Aspects -> Maybe ModuleToSource -> (Text, [Lisp [Char]])
processAnnotations DocTree Aspects
t = \case
  Maybe ModuleToSource
Nothing  -> (, [])                                (Text -> (Text, [Lisp [Char]])) -> Text -> (Text, [Lisp [Char]])
forall a b. (a -> b) -> a -> b
$ DocTree Aspects -> Text
forall ann. DocTree ann -> Text
treeToTextNoAnn DocTree Aspects
t
  Just ModuleToSource
m2s -> (RangeMap Aspects -> [Lisp [Char]])
-> (Text, RangeMap Aspects) -> (Text, [Lisp [Char]])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (ModuleToSource -> RangeMap Aspects -> [Lisp [Char]]
lispifyHighlightingInfo_ ModuleToSource
m2s) ((Text, RangeMap Aspects) -> (Text, [Lisp [Char]]))
-> (Text, RangeMap Aspects) -> (Text, [Lisp [Char]])
forall a b. (a -> b) -> a -> b
$ DocTree Aspects -> (Text, RangeMap Aspects)
forall ann.
(Monoid ann, Null ann) =>
DocTree ann -> (Text, RangeMap ann)
treeToTextWithAnn DocTree Aspects
t