Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Response

Description

Data type for all interactive responses

Synopsis

- data Response
  - = 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)]
  - | Resp_DisplayInfo DisplayInfo
  - | Resp_RunningInfo Int String
  - | Resp_ClearRunningInfo
  - | Resp_ClearHighlighting TokenBased
  - | Resp_DoneAborting
- data RemoveTokenBasedHighlighting
  - = RemoveHighlighting
  - | KeepHighlighting
- data MakeCaseVariant
  - = Function
  - | ExtendedLambda
- data DisplayInfo
  - = Info_CompilationOk String String
  - | Info_Constraints String
  - | Info_AllGoalsWarnings String String String
  - | Info_Time Doc
  - | Info_Error String
  - | Info_Intro Doc
  - | Info_Auto String
  - | 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
- data Status = Status {
  - sShowImplicitArguments :: Bool
  - sChecked :: Bool
  }
- data GiveResult
  - = Give_String String
  - | Give_Paren
  - | Give_NoParen
- type InteractionOutputCallback = Response -> TCM ()
- defaultInteractionOutputCallback :: InteractionOutputCallback

# Documentation

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

Instances

ToJSON MakeCaseVariant Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: MakeCaseVariant -> Value Source # toEncoding :: MakeCaseVariant -> Encoding Source # toJSONList :: [MakeCaseVariant] -> Value Source # toEncodingList :: [MakeCaseVariant] -> Encoding Source #

data DisplayInfo Source #

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 Source # |
Instance details Defined in Agda.Interaction.Response Methods showsPrec :: Int -> DisplayInfo -> ShowS Source # show :: DisplayInfo -> String Source # showList :: [DisplayInfo] -> ShowS Source #
ToJSON DisplayInfo Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: DisplayInfo -> Value Source # toEncoding :: DisplayInfo -> Encoding Source # toJSONList :: [DisplayInfo] -> Value Source # toEncodingList :: [DisplayInfo] -> Encoding Source #

data Status Source #

Status information.

Constructors

Status |

Fields

- sShowImplicitArguments :: Bool

  Are implicit arguments displayed?

- sChecked :: Bool

  Has the module been successfully type checked?

Instances

ToJSON Status Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: Status -> Value Source # toEncoding :: Status -> Encoding Source # toJSONList :: [Status] -> Value Source # toEncodingList :: [Status] -> Encoding Source #

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 |

Instances

ToJSON GiveResult Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: GiveResult -> Value Source # toEncoding :: GiveResult -> Encoding Source # toJSONList :: [GiveResult] -> Value Source # toEncodingList :: [GiveResult] -> Encoding Source #

type InteractionOutputCallback = Response -> TCM () Source #

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

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