| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.EmacsCommand
Description
Code for instructing Emacs to do things
Synopsis
- displayInfo :: String -> DocTree -> Bool -> Maybe ModuleToSource -> Lisp String
- clearRunningInfo :: Lisp String
- displayRunningInfo :: DocTree -> Maybe ModuleToSource -> Lisp String
Documentation
displayInfo :: String -> DocTree -> Bool -> Maybe ModuleToSource -> Lisp String Source #
displayInfo header content append m displays content
with header header in some suitable way in the Agda information buffer.
If append is True, then the content is appended to previous content
(if any), otherwise any previous content is deleted.
If m is Just then ModuleToSourcecontent is rendered with annotations,
otherwise annotations in content are discarded and just the text is displayed.
clearRunningInfo :: Lisp String Source #
Clear the running info buffer.
displayRunningInfo :: DocTree -> Maybe ModuleToSource -> Lisp String Source #
Display running information about what the type-checker is up to.