module Agda.Interaction.EmacsCommand
( Lisp(..)
, response
, putResponse
, display_info'
, clearRunningInfo
, displayRunningInfo
) where
import Agda.Utils.Pretty
import Agda.Utils.String
data Lisp a
= A a
| Cons (Lisp a) (Lisp a)
| L [Lisp a]
| Q (Lisp a)
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 Pretty String where
pretty = text
instance Pretty a => Show (Lisp a) where
show = show . pretty
response :: Lisp String -> String
response = (++ "\n") . map replaceNewLines . show . pretty
where
replaceNewLines '\n' = ' '
replaceNewLines c = c
putResponse :: Lisp String -> IO ()
putResponse = putStr . response
display_info' :: Bool -> String -> String -> Lisp String
display_info' append bufname content =
L [ A "agda2-info-action"
, A (quote bufname)
, A (quote content)
, A (if append then "t" else "nil")
]
runningInfoBufferName :: String
runningInfoBufferName = "*Type-checking*"
clearRunningInfo :: Lisp String
clearRunningInfo =
display_info' False runningInfoBufferName ""
displayRunningInfo :: String -> Lisp String
displayRunningInfo s =
display_info' True runningInfoBufferName s