Agda-2.4.2.4: 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 Source

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) Source 
Pretty a => Pretty (Lisp a) 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

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 Source

Clear the running info buffer.

displayRunningInfo :: String -> Lisp String Source

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