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

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.EmacsCommand

Description

Code for instructing Emacs to do things

Synopsis

- data Lisp a
  - = A a
  - | Cons (Lisp a) (Lisp a)
  - | L [Lisp a]
  - | Q (Lisp a)
- response :: Lisp String -> String
- putResponse :: Lisp String -> IO ()
- display_info' :: Bool -> String -> String -> Lisp String
- clearRunningInfo :: Lisp String
- clearWarning :: Lisp String
- displayRunningInfo :: String -> Lisp String

# Documentation

data Lisp a Source #

Simple Emacs Lisp expressions.

Constructors

A a | Atom.
Cons (Lisp a) (Lisp a) |
L [Lisp a] | List.
Q (Lisp a) |

#### Instances

Instances details

Pretty a => Pretty (Lisp a) Source # |
Instance details Defined in Agda.Interaction.EmacsCommand Methods pretty :: Lisp a -> Doc Source # prettyPrec :: Int -> Lisp a -> Doc Source # prettyList :: [Lisp a] -> Doc Source #
Eq a => Eq (Lisp a) Source # |
Instance details Defined in Agda.Interaction.EmacsCommand Methods (==) :: Lisp a -> Lisp a -> Bool Source # (/=) :: Lisp a -> Lisp a -> Bool Source #

response :: Lisp String -> String Source #

Formats a response command.

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

putResponse :: Lisp String -> IO () Source #

Writes a response command to standard output.

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

clearRunningInfo :: Lisp String Source #

Clear the running info buffer.

clearWarning :: Lisp String Source #

Clear the warning buffer

displayRunningInfo :: String -> Lisp String Source #

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