Module DebugHook.ActionSource

The debugger receives requests by calling read_cmd to get Actions. Each Action may return one or more responses as Answers by calling submit_answer. Many of them return a single Answer or no Answer, but a single step may generate any number of Outputs.

Debugger initialization has the following steps: -> Coq sends Answer.Init <- IDE sends zero or more initialization requests such as Action.UpdBpts <- IDE sends Action.Configd

Stopping in the debugger generates Answer.Prompt and Answer.Goal messages, at which point the IDE will typically call GetStack and GetVars. When the IDE sends with StepIn..Continue, the debugger will execute more code. At that point, Coq won't try to read more messages from the IDE until the debugger stops again or exits.