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 (Maybe ModuleToSource, Doc)
- explainWhyInScope :: MonadPretty m => WhyInScopeData -> m Doc
- prettyResponseContext :: InteractionId -> Bool -> [ResponseContextEntry] -> TCM Doc
- prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
Documentation
namedMetaOf :: OutputConstraint Expr a -> a Source #
showInfoError :: Info_Error -> TCM String Source #
Serializing Info_Error
.
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.
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.