Safe Haskell	None
Language	Haskell2010

Agda.Interaction.EmacsTop

Synopsis

mimicGHCi :: TCM () -> TCM ()
namedMetaOf :: OutputConstraint Expr a -> a
showInfoError :: Info_Error -> TCM String
prettyGoals :: Goals -> TCM Doc
prettyInfoError :: Info_Error -> TCM Doc
explainWhyInScope :: MonadPretty m => WhyInScopeData -> m Doc
prettyResponseContext :: InteractionId -> Bool -> [ResponseContextEntry] -> TCM Doc
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
prettyNormalForm :: CommandState -> ComputeMode -> Expr -> TCM Doc
prettyInferredType :: CommandState -> Expr -> TCM Doc

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.

namedMetaOf :: OutputConstraint Expr a -> a Source #

showInfoError :: Info_Error -> TCM String Source #

Serializing Info_Error.

prettyGoals :: Goals -> TCM Doc Source #

Print open metas nicely.

prettyInfoError :: Info_Error -> TCM Doc Source #

Turn an Info_Error into a Doc.

explainWhyInScope :: MonadPretty m => WhyInScopeData -> m Doc Source #

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.

prettyNormalForm :: CommandState -> ComputeMode -> Expr -> TCM Doc Source #

Pretty-print the result of a compute command in the command state captured when the command completed. Shared with the JSON frontend (Agda.Interaction.JSONTop) so that both frontends render the expression identically.

prettyInferredType :: CommandState -> Expr -> TCM Doc Source #

Pretty-print an inferred type in the command state captured when the inference command completed. Shared with the JSON frontend.