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

module Agda.Interaction.EmacsCommand
  ( Lisp(..)
  , response
  , putResponse
  , display_info'
  , clearRunningInfo
  , clearWarning
  , displayRunningInfo
  ) where

import qualified Data.List as List

import Agda.Utils.Pretty
import Agda.Utils.String

-- | Simple Emacs Lisp expressions.

data Lisp a
  = A a
    -- ^ Atom.
  | Cons (Lisp a) (Lisp a)
    -- Cons cell.
  | L [Lisp a]
    -- ^ List.
  | Q (Lisp a)
    -- Quoted expression.
  deriving Lisp a -> Lisp a -> Bool
(Lisp a -> Lisp a -> Bool)
-> (Lisp a -> Lisp a -> Bool) -> Eq (Lisp a)
forall a. Eq a => Lisp a -> Lisp a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Lisp a -> Lisp a -> Bool
$c/= :: forall a. Eq a => Lisp a -> Lisp a -> Bool
== :: Lisp a -> Lisp a -> Bool
$c== :: forall a. Eq a => Lisp a -> Lisp a -> Bool
Eq

instance Pretty a => Pretty (Lisp a) where
  pretty :: Lisp a -> Doc
pretty (A a
a )     = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
  pretty (Cons Lisp a
a Lisp a
b) = Doc -> Doc
parens (Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty Lisp a
a Doc -> Doc -> Doc
<+> Doc
"." Doc -> Doc -> Doc
<+> Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty Lisp a
b)
  pretty (L [Lisp a]
xs)     = Doc -> Doc
parens ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ((Lisp a -> Doc) -> [Lisp a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty [Lisp a]
xs))
  pretty (Q Lisp a
x)      = Doc
"'" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty Lisp a
x

-- instance Show (Lisp String) where
--   showsPrec _ (A a)      = showString a
--   showsPrec p (Cons a b) = showString "(" . showsPrec p a . showString " . " .
--                                             showsPrec p b . showString ")"
--   showsPrec p (L xs)     = showString "(" . foldr (.) (showString ")")
--                                               (List.intersperse (showString " ")
--                                                  (map (showsPrec p) xs))
--   showsPrec p (Q x)      = showString "'" . showsPrec p x

-- | Formats a response command.
--
--   Replaces @'\n'@ with spaces to ensure that each command is a
--   single line.
response :: Lisp String -> String
response :: Lisp String -> String
response = (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n") (String -> String)
-> (Lisp String -> String) -> Lisp String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
replaceNewLines (String -> String)
-> (Lisp String -> String) -> Lisp String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Lisp String -> Doc) -> Lisp String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lisp String -> Doc
forall a. Pretty a => a -> Doc
pretty
  where
  replaceNewLines :: Char -> Char
replaceNewLines Char
'\n' = Char
' '
  replaceNewLines Char
c    = Char
c

-- | Writes a response command to standard output.

putResponse :: Lisp String -> IO ()
putResponse :: Lisp String -> IO ()
putResponse = String -> IO ()
putStr (String -> IO ())
-> (Lisp String -> String) -> Lisp String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lisp String -> String
response

-- | @displayInBuffer buffername append header content@ displays @content@
-- (with header @header@) in some suitable way in the buffer @buffername@.
-- If @append@ is @True@, then the content is appended to previous content
-- (if any), otherwise any previous content is deleted.

displayInBuffer :: String -> Bool -> String -> String -> Lisp String
displayInBuffer :: String -> Bool -> String -> String -> Lisp String
displayInBuffer String
buffername Bool
append String
header String
content =
    [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A String
buffername
      , 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
content)
      , String -> Lisp String
forall a. a -> Lisp a
A (if Bool
append then String
"t" else String
"nil")
      ]

display_info' :: Bool -> String -> String -> Lisp String
display_info' :: Bool -> String -> String -> Lisp String
display_info' = String -> Bool -> String -> String -> Lisp String
displayInBuffer String
"agda2-info-action"

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

-- | The name of the running info buffer.

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

-- | Clear the running info buffer.

clearRunningInfo :: Lisp String
clearRunningInfo :: Lisp String
clearRunningInfo =
    Bool -> String -> String -> Lisp String
display_info' Bool
False String
runningInfoBufferName String
""

-- | Clear the warning buffer
clearWarning :: Lisp String
clearWarning :: Lisp String
clearWarning = [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-close-warning" ]

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

displayRunningInfo :: String -> Lisp String
displayRunningInfo :: String -> Lisp String
displayRunningInfo String
s =
    Bool -> String -> String -> Lisp String
display_info' Bool
True String
runningInfoBufferName String
s