    module Agda.Interaction.Response
        ( module Agda.Interaction.Response
        , module Agda.Interaction.Response.Base
        , WarningsAndNonFatalErrors
        , InteractionOutputCallback
        , defaultInteractionOutputCallback
        )
        where

    import Agda.Interaction.Response.Base

    import Agda.TypeChecking.Monad.Base
      (TCM, TCErr, TCWarning, InteractionOutputCallback, defaultInteractionOutputCallback)
    import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors)

    --------------------------
    -- * TCM-aware aliases
    --------------------------

    type Response        = Response_boot        TCErr TCWarning WarningsAndNonFatalErrors
    type DisplayInfo     = DisplayInfo_boot     TCErr TCWarning WarningsAndNonFatalErrors
    type Info_Error      = Info_Error_boot      TCErr TCWarning
    type GoalDisplayInfo = GoalDisplayInfo_boot TCErr
    type Goals           = Goals_boot           TCErr