<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Agda.Interaction.Response</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Agda-Interaction-Response.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Interaction-Response.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">Agda-2.3.2.1: A dependently typed functional programming language and proof assistant</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr></table><p class="caption">Agda.Interaction.Response</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Data type for all interactive responses
</p></div></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><span class="keyword">data</span> <a href="#t:Response">Response</a> <ul class="subs"><li>= <a href="#v:Resp_HighlightingInfo">Resp_HighlightingInfo</a> <a href="Agda-Interaction-Highlighting-Precise.html#t:HighlightingInfo">HighlightingInfo</a> <a href="Agda-Interaction-FindFile.html#t:ModuleToSource">ModuleToSource</a> </li><li>| <a href="#v:Resp_Status">Resp_Status</a> <a href="Agda-Interaction-Response.html#t:Status">Status</a> </li><li>| <a href="#v:Resp_JumpToError">Resp_JumpToError</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int32">Int32</a> </li><li>| <a href="#v:Resp_InteractionPoints">Resp_InteractionPoints</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:InteractionId">InteractionId</a>] </li><li>| <a href="#v:Resp_GiveAction">Resp_GiveAction</a> <a href="Agda-TypeChecking-Monad-Base.html#t:InteractionId">InteractionId</a> <a href="Agda-Interaction-Response.html#t:GiveResult">GiveResult</a> </li><li>| <a href="#v:Resp_MakeCaseAction">Resp_MakeCaseAction</a> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>] </li><li>| <a href="#v:Resp_MakeCase">Resp_MakeCase</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>] </li><li>| <a href="#v:Resp_SolveAll">Resp_SolveAll</a> [(<a href="Agda-TypeChecking-Monad-Base.html#t:InteractionId">InteractionId</a>, <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)] </li><li>| <a href="#v:Resp_DisplayInfo">Resp_DisplayInfo</a> <a href="Agda-Interaction-Response.html#t:DisplayInfo">DisplayInfo</a> </li><li>| <a href="#v:Resp_RunningInfo">Resp_RunningInfo</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> </li><li>| <a href="#v:Resp_ClearRunningInfo">Resp_ClearRunningInfo</a> </li><li>| <a href="#v:Resp_ClearHighlighting">Resp_ClearHighlighting</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:DisplayInfo">DisplayInfo</a> <ul class="subs"><li>= <a href="#v:Info_CompilationOk">Info_CompilationOk</a> </li><li>| <a href="#v:Info_Constraints">Info_Constraints</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> </li><li>| <a href="#v:Info_AllGoals">Info_AllGoals</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> </li><li>| <a href="#v:Info_Error">Info_Error</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> </li><li>| <a href="#v:Info_Intro">Info_Intro</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a> </li><li>| <a href="#v:Info_Auto">Info_Auto</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> </li><li>| <a href="#v:Info_ModuleContents">Info_ModuleContents</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a> </li><li>| <a href="#v:Info_NormalForm">Info_NormalForm</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a> </li><li>| <a href="#v:Info_GoalType">Info_GoalType</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a> </li><li>| <a href="#v:Info_CurrentGoal">Info_CurrentGoal</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a> </li><li>| <a href="#v:Info_InferredType">Info_InferredType</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a> </li><li>| <a href="#v:Info_Context">Info_Context</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:Status">Status</a> = <a href="#v:Status">Status</a> {<ul class="subs"><li><a href="#v:sShowImplicitArguments">sShowImplicitArguments</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:sChecked">sChecked</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li></ul>}</li><li class="src short"><span class="keyword">data</span> <a href="#t:GiveResult">GiveResult</a> <ul class="subs"><li>= <a href="#v:Give_String">Give_String</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> </li><li>| <a href="#v:Give_Paren">Give_Paren</a> </li><li>| <a href="#v:Give_NoParen">Give_NoParen</a> </li></ul></li><li class="src short"><span class="keyword">type</span> <a href="#t:InteractionOutputCallback">InteractionOutputCallback</a> = <a href="Agda-Interaction-Response.html#t:Response">Response</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:defaultInteractionOutputCallback">defaultInteractionOutputCallback</a> :: <a href="Agda-Interaction-Response.html#t:InteractionOutputCallback">InteractionOutputCallback</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Response" class="def">Response</a> <a href="src/Agda-Interaction-Response.html#Response" class="link">Source</a></p><div class="doc"><p>Responses for any interactive interface
</p><p>Note that the response is given in pieces and incrementally,
so the user can have timely response even during long computations.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Resp_HighlightingInfo" class="def">Resp_HighlightingInfo</a> <a href="Agda-Interaction-Highlighting-Precise.html#t:HighlightingInfo">HighlightingInfo</a> <a href="Agda-Interaction-FindFile.html#t:ModuleToSource">ModuleToSource</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Resp_Status" class="def">Resp_Status</a> <a href="Agda-Interaction-Response.html#t:Status">Status</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Resp_JumpToError" class="def">Resp_JumpToError</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int32">Int32</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Resp_InteractionPoints" class="def">Resp_InteractionPoints</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:InteractionId">InteractionId</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Resp_GiveAction" class="def">Resp_GiveAction</a> <a href="Agda-TypeChecking-Monad-Base.html#t:InteractionId">InteractionId</a> <a href="Agda-Interaction-Response.html#t:GiveResult">GiveResult</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Resp_MakeCaseAction" class="def">Resp_MakeCaseAction</a> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Resp_MakeCase" class="def">Resp_MakeCase</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Resp_SolveAll" class="def">Resp_SolveAll</a> [(<a href="Agda-TypeChecking-Monad-Base.html#t:InteractionId">InteractionId</a>, <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Resp_DisplayInfo" class="def">Resp_DisplayInfo</a> <a href="Agda-Interaction-Response.html#t:DisplayInfo">DisplayInfo</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Resp_RunningInfo" class="def">Resp_RunningInfo</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Resp_ClearRunningInfo" class="def">Resp_ClearRunningInfo</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Resp_ClearHighlighting" class="def">Resp_ClearHighlighting</a></td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:DisplayInfo" class="def">DisplayInfo</a> <a href="src/Agda-Interaction-Response.html#DisplayInfo" class="link">Source</a></p><div class="doc"><p>Info to display at the end of an interactive command
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Info_CompilationOk" class="def">Info_CompilationOk</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Info_Constraints" class="def">Info_Constraints</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Info_AllGoals" class="def">Info_AllGoals</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Info_Error" class="def">Info_Error</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></td><td class="doc"><p>When an error message is displayed this constructor should be
used, if appropriate.
</p></td></tr><tr><td class="src"><a name="v:Info_Intro" class="def">Info_Intro</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a></td><td class="doc"><p><code><a href="Agda-Interaction-Response.html#v:Info_Intro">Info_Intro</a></code> denotes two different types of errors
TODO: split these into separate constructors
</p></td></tr><tr><td class="src"><a name="v:Info_Auto" class="def">Info_Auto</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></td><td class="doc"><p><code><a href="Agda-Interaction-Response.html#v:Info_Auto">Info_Auto</a></code> denotes either an error or a success (when <code><a href="Agda-Interaction-Response.html#v:Resp_GiveAction">Resp_GiveAction</a></code> is present)
TODO: split these into separate constructors
</p></td></tr><tr><td class="src"><a name="v:Info_ModuleContents" class="def">Info_ModuleContents</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Info_NormalForm" class="def">Info_NormalForm</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Info_GoalType" class="def">Info_GoalType</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Info_CurrentGoal" class="def">Info_CurrentGoal</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Info_InferredType" class="def">Info_InferredType</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Info_Context" class="def">Info_Context</a> <a href="/usr/share/doc/ghc/html/libraries/pretty-1.1.1.0/Text-PrettyPrint.html#t:Doc">Doc</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:DisplayInfo" class="caption collapser" onclick="toggleSection('i:DisplayInfo')">Instances</p><div id="section.i:DisplayInfo" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Interaction-Response.html#t:DisplayInfo">DisplayInfo</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Status" class="def">Status</a> <a href="src/Agda-Interaction-Response.html#Status" class="link">Source</a></p><div class="doc"><p>Status information.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Status" class="def">Status</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:sShowImplicitArguments" class="def">sShowImplicitArguments</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc"><p>Are implicit arguments displayed?
</p></dd><dt class="src"><a name="v:sChecked" class="def">sChecked</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc"><p>Has the module been successfully type checked?
</p></dd></dl><div class="clear"></div></div></td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:GiveResult" class="def">GiveResult</a> <a href="src/Agda-Interaction-Response.html#GiveResult" class="link">Source</a></p><div class="doc"><p>Give action result
</p><p>Comment derived from agda2-mode.el
</p><p>If <code><a href="Agda-Interaction-Response.html#t:GiveResult">GiveResult</a></code> is 'Give_String s', then the goal is replaced by <code>s</code>,
and otherwise the text inside the goal is retained (parenthesised
if <code><a href="Agda-Interaction-Response.html#t:GiveResult">GiveResult</a></code> is <code><a href="Agda-Interaction-Response.html#v:Give_Paren">Give_Paren</a></code>).
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Give_String" class="def">Give_String</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Give_Paren" class="def">Give_Paren</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Give_NoParen" class="def">Give_NoParen</a></td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:InteractionOutputCallback" class="def">InteractionOutputCallback</a> = <a href="Agda-Interaction-Response.html#t:Response">Response</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Interaction-Response.html#InteractionOutputCallback" class="link">Source</a></p><div class="doc"><p>Callback fuction to call when there is a response
to give to the interactive frontend.
</p><p>Note that the response is given in pieces and incrementally,
so the user can have timely response even during long computations.
</p><p>Typical <code><a href="Agda-Interaction-Response.html#t:InteractionOutputCallback">InteractionOutputCallback</a></code> functions:
</p><ul><li> Convert the response into a <code><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></code> representation and
print it on standard output
(suitable for inter-process communication).
</li><li> Put the response into a mutable variable stored in the
closure of the <code><a href="Agda-Interaction-Response.html#t:InteractionOutputCallback">InteractionOutputCallback</a></code> function.
(suitable for intra-process communication).
</li></ul></div></div><div class="top"><p class="src"><a name="v:defaultInteractionOutputCallback" class="def">defaultInteractionOutputCallback</a> :: <a href="Agda-Interaction-Response.html#t:InteractionOutputCallback">InteractionOutputCallback</a><a href="src/Agda-Interaction-Response.html#defaultInteractionOutputCallback" class="link">Source</a></p><div class="doc"><p>The default <code><a href="Agda-Interaction-Response.html#t:InteractionOutputCallback">InteractionOutputCallback</a></code> function
is set to <code>__</code><code>IMPOSSIBLE__</code> because in this way it is easier to
recognize that some response is lost due to an uninitialized
<code><a href="Agda-Interaction-Response.html#t:InteractionOutputCallback">InteractionOutputCallback</a></code> function.
</p></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>
