module Agda.Interaction.EmacsCommand
( Lisp(..)
, response
, putResponse
, display_info'
, clearRunningInfo
, clearWarning
, displayRunningInfo
) where
import Agda.Syntax.Common.Pretty
import Agda.Utils.String
data Lisp a
= A a
| Cons (Lisp a) (Lisp a)
| L [Lisp a]
| Q (Lisp a)
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
$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
/= :: 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
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"." Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> 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
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
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 :: 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"
runningInfoBufferName :: String
runningInfoBufferName :: String
runningInfoBufferName = String
"*Type-checking*"
clearRunningInfo :: Lisp String
clearRunningInfo :: Lisp String
clearRunningInfo =
Bool -> String -> String -> Lisp String
display_info' Bool
False String
runningInfoBufferName String
""
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" ]
displayRunningInfo :: String -> Lisp String
displayRunningInfo :: String -> Lisp String
displayRunningInfo String
s =
Bool -> String -> String -> Lisp String
display_info' Bool
True String
runningInfoBufferName String
s