Agda-2.5.4: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.EmacsCommand

Description

Code for instructing Emacs to do things

Synopsis

Documentation

data Lisp a #

Simple Emacs Lisp expressions.

Constructors

A a

Atom.

Cons (Lisp a) (Lisp a) 
L [Lisp a]

List.

Q (Lisp a) 
Instances
Eq a => Eq (Lisp a) # 
Instance details

Defined in Agda.Interaction.EmacsCommand

Methods

(==) :: Lisp a -> Lisp a -> Bool #

(/=) :: Lisp a -> Lisp a -> Bool #

Show (Lisp String) # 
Instance details

Defined in Agda.Interaction.EmacsCommand

Methods

showsPrec :: Int -> Lisp String -> ShowS #

show :: Lisp String -> String #

showList :: [Lisp String] -> ShowS #

Pretty a => Pretty (Lisp a) # 
Instance details

Defined in Agda.Interaction.EmacsCommand

Methods

pretty :: Lisp a -> Doc #

prettyPrec :: Int -> Lisp a -> Doc #

prettyList :: [Lisp a] -> Doc #

response :: Lisp String -> String #

Formats a response command.

Replaces '\n' with spaces to ensure that each command is a single line.

putResponse :: Lisp String -> IO () #

Writes a response command to standard output.

display_info' :: Bool -> String -> String -> Lisp String #

display_warning :: String -> String -> Lisp String #

clearRunningInfo :: Lisp String #

Clear the running info buffer.

clearWarning :: Lisp String #

Clear the warning buffer

displayRunningInfo :: String -> Lisp String #

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