ModuleAgda-2.8.0.2Haskell2010

Agda.Interaction.Response.Base

Data type for all interactive responses

11 types

PackageAgda-2.8.0.2
Exports11
LanguageHaskell2010
LicenceMIT
SourceBase.hs

datadata Response_boot tcErr tcWarning warningsAndNonFatalErrors

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

Instances1EncodeTCM

EncodeTCM ResponseDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan

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

datadata MakeCaseVariant

There are two kinds of "make case" commands.

Function ExtendedLambda

Instances2ToJSON, EncodeTCM

ToJSON MakeCaseVariantDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
EncodeTCM MakeCaseVariantDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan

datadata DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors

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)

Instances1EncodeTCM

EncodeTCM DisplayInfoDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan

datadata GoalDisplayInfo_boot tcErr

Constructors

Goal_HelperFunction (OutputConstraint' Expr Expr)
Goal_NormalForm ComputeMode Expr
Goal_GoalType Rewrite GoalTypeAux [ResponseContextEntry] [IPFace' Expr] [OutputForm_boot tcErr Expr Expr]
Goal_CurrentGoal Rewrite
Goal_InferredType Expr

typetype Goals_boot tcErr = ([OutputConstraint_boot tcErr Expr InteractionId], [OutputConstraint_boot tcErr Expr NamedMeta])

Goals & Warnings

datadata Info_Error_boot tcErr tcWarning

Errors that goes into Info_Error

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

Constructors

Info_GenericError tcErr
Info_CompilationError (Set tcWarning)
Info_HighlightingParseError InteractionId
Info_HighlightingScopeCheckError InteractionId

Instances1EncodeTCM

EncodeTCM Info_ErrorDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan

datadata GoalTypeAux

Auxiliary information that comes with Goal Type

Constructors

GoalOnly
GoalAndHave Expr [IPFace' Expr]
GoalAndElaboration Expr

Instances1EncodeTCM

EncodeTCM GoalTypeAuxDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan

datadata ResponseContextEntry

Entry in context.

Constructors

ResponseContextEntry
- respOrigName :: Name
  The original concrete name.
- respReifName :: Name
  The name reified from abstract syntax.
- respType :: Arg Expr
  The type.
- respLetValue :: Maybe Expr
  The value (if it is a let-bound variable)
- respInScope :: NameInScope
  Whether the respReifName is in scope.

Instances1EncodeTCM

EncodeTCM ResponseContextEntryDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan

datadata Status

Status information.

Constructors

Status
- sShowImplicitArguments :: Bool
  Are implicit arguments displayed?
- sShowIrrelevantArguments :: Bool
  Are irrelevant arguments displayed?
- sChecked :: Bool
  Has the module been successfully type checked?

Instances2ToJSON, EncodeTCM

ToJSON StatusDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
EncodeTCM StatusDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan

datadata 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

Instances2ToJSON, EncodeTCM

ToJSON GiveResultDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
EncodeTCM GiveResultDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan