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

module Agda.Interaction.EmacsCommand
  ( displayInfo
  , clearRunningInfo
  , displayRunningInfo
  ) 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 :: String -> DocTree -> Bool -> Maybe ModuleToSource -> Lisp String
displayInfo String
header DocTree
content Bool
append Maybe ModuleToSource
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
$ [[Lisp String]] -> [Lisp String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-info-action"
    , String -> Lisp String
forall a. a -> Lisp a
A (String -> String
quote String
header)
    , String -> Lisp String
forall a. a -> Lisp a
A (String -> String
quote (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Text -> String
Text.unpack Text
t)
    , String -> Lisp String
forall a. a -> Lisp a
A (if Bool
append then String
"t" else String
"nil")
    ]
  , (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]
ann
  ]
  where
    (Text
t, [Lisp String]
ann) = case Maybe ModuleToSource
m of
      Maybe ModuleToSource
Nothing  -> (, [])                                (Text -> (Text, [Lisp String])) -> Text -> (Text, [Lisp String])
forall a b. (a -> b) -> a -> b
$ DocTree -> Text
forall ann. DocTree ann -> Text
treeToTextNoAnn   DocTree
content
      Just ModuleToSource
m2s -> (HighlightingInfo -> [Lisp String])
-> (Text, HighlightingInfo) -> (Text, [Lisp String])
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 -> HighlightingInfo -> [Lisp String]
lispifyHighlightingInfo_ ModuleToSource
m2s) ((Text, HighlightingInfo) -> (Text, [Lisp String]))
-> (Text, HighlightingInfo) -> (Text, [Lisp String])
forall a b. (a -> b) -> a -> b
$ DocTree -> (Text, HighlightingInfo)
forall ann.
(Monoid ann, Null ann) =>
DocTree ann -> (Text, RangeMap ann)
treeToTextWithAnn DocTree
content

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

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

runningInfoHeader :: String
runningInfoHeader :: String
runningInfoHeader = String
"*Type-checking*"

-- | Clear the running info buffer.

clearRunningInfo :: Lisp String
clearRunningInfo :: Lisp String
clearRunningInfo = String -> DocTree -> Bool -> Maybe ModuleToSource -> Lisp String
displayInfo String
runningInfoHeader DocTree
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 -> Maybe ModuleToSource -> Lisp String
displayRunningInfo DocTree
t = String -> DocTree -> Bool -> Maybe ModuleToSource -> Lisp String
displayInfo String
runningInfoHeader DocTree
t Bool
True