Agda-2.7.0: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Interaction.Response

Synopsis

Documentation

data WarningsAndNonFatalErrors Source #

Assorted warnings and errors to be displayed to the user

Instances

Instances details
EncodeTCM DisplayInfo Source # 
Instance details

Defined in Agda.Interaction.JSONTop

EncodeTCM Response Source # 
Instance details

Defined in Agda.Interaction.JSONTop

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).