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

Agda.Interaction.Response

Description

Data type for all interactive responses

Synopsis

Documentation

data Response Source #

Responses for any interactive interface

Note that the response is given in pieces and incrementally, so the user can have timely response even during long computations.

Constructors

Resp_HighlightingInfo HighlightingInfo RemoveTokenBasedHighlighting HighlightingMethod ModuleToSource 
Resp_Status Status 
Resp_JumpToError FilePath Int32 
Resp_InteractionPoints [InteractionId] 
Resp_GiveAction InteractionId GiveResult 
Resp_MakeCase InteractionId MakeCaseVariant [String]

Response is list of printed clauses.

Resp_SolveAll [(InteractionId, Expr)]

Solution for one or more meta-variables.

Resp_DisplayInfo DisplayInfo 
Resp_RunningInfo Int String

The integer is the message's debug level.

Resp_ClearRunningInfo 
Resp_ClearHighlighting TokenBased

Clear highlighting of the given kind.

Resp_DoneAborting

A command sent when an abort command has completed successfully.

Resp_DoneExiting

A command sent when an exit command is about to be completed.

Instances

Instances details
EncodeTCM Response Source # 
Instance details

Defined in Agda.Interaction.JSONTop

data RemoveTokenBasedHighlighting Source #

Should token-based highlighting be removed in conjunction with the application of new highlighting (in order to reduce the risk of flicker)?

Constructors

RemoveHighlighting

Yes, remove all token-based highlighting from the file.

KeepHighlighting

No.

data MakeCaseVariant Source #

There are two kinds of "make case" commands.

Constructors

Function 
ExtendedLambda 

data WarningsAndNonFatalErrors Source #

Assorted warnings and errors to be displayed to the user

data Info_Error Source #

Errors that goes into Info_Error

When an error message is displayed this constructor should be used, if appropriate.

Instances

Instances details
EncodeTCM Info_Error Source # 
Instance details

Defined in Agda.Interaction.JSONTop

data GoalTypeAux Source #

Auxiliary information that comes with Goal Type

Instances

Instances details
EncodeTCM GoalTypeAux Source # 
Instance details

Defined in Agda.Interaction.JSONTop

data ResponseContextEntry Source #

Entry in context.

Constructors

ResponseContextEntry 

Fields

Instances

Instances details
EncodeTCM ResponseContextEntry Source # 
Instance details

Defined in Agda.Interaction.JSONTop

data Status Source #

Status information.

Constructors

Status 

Fields

Instances

Instances details
EncodeTCM Status Source # 
Instance details

Defined in Agda.Interaction.JSONTop

ToJSON Status Source # 
Instance details

Defined in Agda.Interaction.JSONTop

data GiveResult Source #

Give action result

Comment derived from agda2-mode.el

If GiveResult is 'Give_String s', then the goal is replaced by s, and otherwise the text inside the goal is retained (parenthesised if GiveResult is Give_Paren).

type InteractionOutputCallback = Response -> 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 Aspect 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).