Safe Haskell | None |
---|---|
Language | Haskell98 |
Data type for all interactive responses
- data Response
- = Resp_HighlightingInfo HighlightingInfo 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
- data MakeCaseVariant
- data DisplayInfo
- = Info_CompilationOk
- | Info_Constraints String
- | Info_AllGoals String
- | Info_Error String
- | Info_Intro Doc
- | Info_Auto String
- | Info_ModuleContents 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 {}
- data GiveResult
- type InteractionOutputCallback = Response -> TCM ()
- defaultInteractionOutputCallback :: InteractionOutputCallback
Documentation
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.
data DisplayInfo Source
Info to display at the end of an interactive command
Info_CompilationOk | |
Info_Constraints String | |
Info_AllGoals String | |
Info_Error String | When an error message is displayed this constructor should be used, if appropriate. |
Info_Intro Doc |
|
Info_Auto String |
|
Info_ModuleContents Doc | |
Info_WhyInScope Doc | |
Info_NormalForm Doc | |
Info_GoalType Doc | |
Info_CurrentGoal Doc | |
Info_InferredType Doc | |
Info_Context Doc | |
Info_HelperFunction Doc | |
Info_Version |
Status information.
Status | |
|
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
).
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
String
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).