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 RemoveTokenBasedHighlighting HighlightingMethod ModuleToSource

Resp_Status Status

Resp_JumpToError FilePath Int32

Resp_InteractionPoints [InteractionId]

Resp_GiveAction InteractionId GiveResult

Resp_MakeCase MakeCaseVariant [String]

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.

data RemoveTokenBasedHighlighting

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

There are two kinds of "make case" commands.

Constructors

Function

ExtendedLambda

Instances

ToJSON MakeCaseVariant

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: MakeCaseVariant -> Value

toEncoding :: MakeCaseVariant -> Encoding

toJSONList :: [MakeCaseVariant] -> Value

toEncodingList :: [MakeCaseVariant] -> Encoding

data DisplayInfo

Info to display at the end of an interactive command

Constructors

Info_CompilationOk String String

Strings are the warnings and the (non-fatal) errors

Info_Constraints String

Info_AllGoalsWarnings String String String

Strings are the goals, the warnings and the (non-fatal) errors

Info_Time Doc

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_SearchAbout 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

Defined in Agda.Interaction.Response

Methods

showsPrec :: Int -> DisplayInfo -> ShowS

show :: DisplayInfo -> String

showList :: [DisplayInfo] -> ShowS

ToJSON DisplayInfo

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: DisplayInfo -> Value

toEncoding :: DisplayInfo -> Encoding

toJSONList :: [DisplayInfo] -> Value

toEncodingList :: [DisplayInfo] -> Encoding

data Status

Status information.

Constructors

Status

Fields

• sShowImplicitArguments :: Bool

  Are implicit arguments displayed?

• sChecked :: Bool

  Has the module been successfully type checked?

Instances

ToJSON Status

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Status -> Value

toEncoding :: Status -> Encoding

toJSONList :: [Status] -> Value

toEncodingList :: [Status] -> Encoding

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

Instances

ToJSON GiveResult

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: GiveResult -> Value

toEncoding :: GiveResult -> Encoding

toJSONList :: [GiveResult] -> Value

toEncodingList :: [GiveResult] -> Encoding

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

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