module Agda.Interaction.EmacsCommand
( Lisp(..)
, putResponse
) where
import qualified Agda.Utils.IO.Locale as LocIO
import Agda.Utils.Pretty
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 l = show (text "agda2_mode_code" <+> pretty l)
putResponse :: Lisp String -> IO ()
putResponse = LocIO.putStrLn . response