Agda.Interaction.Response

Documentation

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

Assorted warnings and errors to be displayed to the user

Instances

EncodeTCM DisplayInfo

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: DisplayInfo -> TCM Value

EncodeTCM Response

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Response -> TCM Value

type InteractionOutputCallback = Response_boot TCErr TCWarning WarningsAndNonFatalErrors -> TCM ()

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

The default InteractionOutputCallback function prints certain things to stdout (other things generate internal errors).