Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.Response.Base

Description

Data type for all interactive responses

Synopsis

Documentation

data Response_boot tcErr tcWarning warningsAndNonFatalErrors 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_Mimer InteractionId (Maybe String) 
Resp_DisplayInfo (DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors) 
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 DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors Source #

Info to display at the end of an interactive command

Constructors

Info_CompilationOk CompilerBackend warningsAndNonFatalErrors 
Info_Constraints [OutputForm_boot tcErr Expr Expr] 
Info_AllGoalsWarnings (Goals_boot tcErr) warningsAndNonFatalErrors 
Info_Time CPUTime 
Info_Error (Info_Error_boot tcErr tcWarning)

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

Info_Intro_NotFound 
Info_Intro_ConstructorUnknown [String] 
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 [Name] Telescope [(Name, Type)] 
Info_SearchAbout [(Name, Type)] String 
Info_WhyInScope WhyInScopeData 
Info_NormalForm CommandState ComputeMode (Maybe CPUTime) Expr 
Info_InferredType CommandState (Maybe CPUTime) Expr 
Info_Context InteractionId [ResponseContextEntry] 
Info_Version 
Info_GoalSpecific InteractionId (GoalDisplayInfo_boot tcErr) 

Instances

Instances details
EncodeTCM DisplayInfo Source # 
Instance details

Defined in Agda.Interaction.JSONTop

data Info_Error_boot tcErr tcWarning 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).

Constructors

Give_String String 
Give_Paren 
Give_NoParen