Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.EmacsTop

Synopsis

Documentation

mimicGHCi :: TCM () -> TCM () Source #

mimicGHCi is a fake ghci interpreter for the Emacs frontend and for interaction tests.

mimicGHCi reads the Emacs frontend commands from stdin, interprets them and print the result into stdout.

prettyGoals :: Goals -> TCM Doc Source #

Print open metas nicely.

prettyInfoError :: Info_Error -> TCM (Maybe ModuleToSource, Doc) Source #

Turn an Info_Error into a Doc. Possibly returns a ModuleToSource appropriate for rendering the returned Doc.

A Nothing return only indicates that the Doc can be safely rendered in the current TC state. Pass this value to wantBufferHighlighting to respect whether the user wants syntax colouring.

prettyResponseContext Source #

Arguments

:: InteractionId

Context of this meta-variable.

-> Bool

Print the elements in reverse order?

-> [ResponseContextEntry] 
-> TCM Doc 

Pretty-prints the context of the given meta-variable.

prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc Source #

Pretty-prints the type of the meta-variable.