Agda.Interaction.Response

Data type for all interactive responses

Documentation

data Response

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 ModuleToSource

Resp_Status Status

Resp_JumpToError FilePath Int32

Resp_InteractionPoints [InteractionId]

Resp_GiveAction InteractionId GiveResult

Resp_MakeCase MakeCaseVariant [String]

Resp_SolveAll [(InteractionId, Expr)]

Resp_DisplayInfo DisplayInfo

Resp_RunningInfo Int String

The integer is the message's debug level.

Resp_ClearRunningInfo

Resp_ClearHighlighting

data MakeCaseVariant

There are two kinds of "make case" commands.

Constructors

Function

ExtendedLambda

data DisplayInfo

Info to display at the end of an interactive command

Constructors

Info_CompilationOk

Info_Constraints String

Info_AllGoals String

Info_Error String

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

Info_Intro Doc

Info_Intro denotes two different types of errors TODO: split these into separate constructors

Info_Auto String

Info_Auto denotes either an error or a success (when Resp_GiveAction is present) TODO: split these into separate constructors

Info_ModuleContents Doc

Info_WhyInScope Doc

Info_NormalForm Doc

Info_GoalType Doc

Info_CurrentGoal Doc

Info_InferredType Doc

Info_Context Doc

Info_HelperFunction Doc

Info_Version

Instances

Show DisplayInfo

data Status

Status information.

Constructors

Status

Fields

sShowImplicitArguments :: Bool

Are implicit arguments displayed?

sChecked :: Bool

Has the module been successfully type checked?

data GiveResult

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

Constructors

Give_String String

Give_Paren

Give_NoParen

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