module Agda.Interaction.Response
( Response (..)
, MakeCaseVariant (..)
, DisplayInfo (..)
, Status (..)
, GiveResult (..)
, InteractionOutputCallback
, defaultInteractionOutputCallback
) where
import Agda.Interaction.Highlighting.Precise
import Agda.TypeChecking.Monad.Base
import Agda.Syntax.Common (InteractionId(..))
import Agda.Syntax.Concrete (Expr)
import Agda.Utils.Pretty
import Control.Monad.Trans
import Data.Int
import System.IO
#include "undefined.h"
import Agda.Utils.Impossible
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 = Function | ExtendedLambda
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
deriving Show
data Status = Status
{ sShowImplicitArguments :: Bool
, sChecked :: Bool
}
data GiveResult
= Give_String String
| Give_Paren
| Give_NoParen
type InteractionOutputCallback = Response -> TCM ()
defaultInteractionOutputCallback :: InteractionOutputCallback
defaultInteractionOutputCallback r = case r of
Resp_HighlightingInfo {} -> __IMPOSSIBLE__
Resp_Status {} -> __IMPOSSIBLE__
Resp_JumpToError {} -> __IMPOSSIBLE__
Resp_InteractionPoints {} -> __IMPOSSIBLE__
Resp_GiveAction {} -> __IMPOSSIBLE__
Resp_MakeCase {} -> __IMPOSSIBLE__
Resp_SolveAll {} -> __IMPOSSIBLE__
Resp_DisplayInfo {} -> __IMPOSSIBLE__
Resp_RunningInfo _ s -> liftIO $ do
putStr s
hFlush stdout
Resp_ClearRunningInfo {} -> __IMPOSSIBLE__
Resp_ClearHighlighting {} -> __IMPOSSIBLE__