ModuleAgda-2.8.0.2Haskell2010

Agda.Interaction.Response.Base

Data type for all interactive responses

Synopsis

data Response_boot
data RemoveTokenBasedHighlighting
data MakeCaseVariant
data DisplayInfo_boot
data GoalDisplayInfo_boot
type Goals_boot
data Info_Error_boot
data GoalTypeAux
data ResponseContextEntry
data Status
data GiveResult

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

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.

datadata MakeCaseVariant

Source#

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

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)

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

Source#

Goals & Warnings

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

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

Source#

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

Source#

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

Source#

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

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

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