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

Safe HaskellNone
LanguageHaskell98

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

Pretty a => Show (Lisp a) 
Pretty a => Pretty (Lisp a) 

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_info' append header content displays content (with header header) in some suitable way. If append is True, then the content is appended to previous content (if any), otherwise any previous content is deleted.

clearRunningInfo :: Lisp String

Clear the running info buffer.

displayRunningInfo :: String -> Lisp String

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