Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- type Response = Response_boot TCErr TCWarning WarningsAndNonFatalErrors
- type Goals = Goals_boot TCErr
- type Info_Error = Info_Error_boot TCErr TCWarning
- type DisplayInfo = DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
- type GoalDisplayInfo = GoalDisplayInfo_boot TCErr
- module Agda.Interaction.Response.Base
- data WarningsAndNonFatalErrors
- type InteractionOutputCallback = Response_boot TCErr TCWarning WarningsAndNonFatalErrors -> TCM ()
- defaultInteractionOutputCallback :: InteractionOutputCallback
Documentation
type Goals = Goals_boot TCErr Source #
type Info_Error = Info_Error_boot TCErr TCWarning Source #
data WarningsAndNonFatalErrors Source #
Assorted warnings and errors to be displayed to the user
type InteractionOutputCallback = Response_boot TCErr TCWarning WarningsAndNonFatalErrors -> TCM () Source #
Callback fuction to call when there is a response to give to the interactive frontend.
Note that the response is given in pieces and incrementally, so the user can have timely response even during long computations.
Typical InteractionOutputCallback
functions:
- Convert the response into a
String
representation and print it on standard output (suitable for inter-process communication). - Put the response into a mutable variable stored in the
closure of the
InteractionOutputCallback
function. (suitable for intra-process communication).
defaultInteractionOutputCallback :: InteractionOutputCallback Source #
The default InteractionOutputCallback
function prints certain
things to stdout (other things generate internal errors).