Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Interaction.Response
Synopsis
- type DisplayInfo = DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
- type GoalDisplayInfo = GoalDisplayInfo_boot TCErr
- type Goals = Goals_boot TCErr
- type Info_Error = Info_Error_boot TCErr TCWarning
- type Response = Response_boot TCErr TCWarning WarningsAndNonFatalErrors
- 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
Instances
EncodeTCM DisplayInfo Source # | |
Defined in Agda.Interaction.JSONTop | |
EncodeTCM Response Source # | |
Null WarningsAndNonFatalErrors Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods empty :: WarningsAndNonFatalErrors Source # null :: WarningsAndNonFatalErrors -> Bool Source # |
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).