{-# LANGUAGE CPP #-}
module Agda.Interaction.EmacsCommand
( Lisp(..)
, response
, putResponse
, display_info'
, display_warning
, clearRunningInfo
, clearWarning
, displayRunningInfo
) where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ((<>))
#endif
import qualified Data.List as List
import Agda.Utils.Pretty
import Agda.Utils.String
data Lisp a
= A a
| Cons (Lisp a) (Lisp a)
| L [Lisp a]
| Q (Lisp a)
deriving Eq
instance Pretty a => Pretty (Lisp a) where
pretty (A a ) = pretty a
pretty (Cons a b) = parens (pretty a <+> text "." <+> pretty b)
pretty (L xs) = parens (hsep (map pretty xs))
pretty (Q x) = text "'" <> pretty 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
response :: Lisp String -> String
response = (++ "\n") . map replaceNewLines . show . pretty
where
replaceNewLines '\n' = ' '
replaceNewLines c = c
putResponse :: Lisp String -> IO ()
putResponse = putStr . response
displayInBuffer :: String -> Bool -> String -> String -> Lisp String
displayInBuffer buffername append header content =
L [ A buffername
, A (quote header)
, A (quote content)
, A (if append then "t" else "nil")
]
display_info' :: Bool -> String -> String -> Lisp String
display_info' = displayInBuffer "agda2-info-action"
display_warning :: String -> String -> Lisp String
display_warning = displayInBuffer "agda2-warning-action" False
runningInfoBufferName :: String
runningInfoBufferName = "*Type-checking*"
clearRunningInfo :: Lisp String
clearRunningInfo =
display_info' False runningInfoBufferName ""
clearWarning :: Lisp String
clearWarning = L [ A "agda2-close-warning" ]
displayRunningInfo :: String -> Lisp String
displayRunningInfo s =
display_info' True runningInfoBufferName s