    {-# LANGUAGE NondecreasingIndentation #-}
    {-# OPTIONS_GHC -fno-cse #-}
    {-# OPTIONS_GHC -fno-warn-orphans #-}

    module Agda.Interaction.InteractionTop
      ( module Agda.Interaction.InteractionTop
      )
      where

    import Prelude hiding (null)

    import Control.Concurrent
    import Control.Concurrent.Async
    import Control.Concurrent.STM.TChan
    import Control.Concurrent.STM.TVar

    import qualified Control.Exception  as E

    import Control.Monad
    import Control.Monad.Except         ( MonadError(..), ExceptT(..), runExceptT )
    import Control.Monad.IO.Class       ( MonadIO(..) )
    import Control.Monad.Fail           ( MonadFail )
    import Control.Monad.State          ( MonadState(..), gets, modify, runStateT )
    import Control.Monad.STM
    import Control.Monad.Trans          ( lift )

    import qualified Data.Char as Char
    import Data.Function
    import qualified Data.List as List
    import qualified Data.Map as Map
    import Data.Maybe

    import System.Directory
    import System.FilePath

    import Agda.TypeChecking.Monad as TCM
      hiding (initState, setCommandLineOptions)
    import qualified Agda.TypeChecking.Monad as TCM
    import qualified Agda.TypeChecking.Pretty as TCP
    import Agda.TypeChecking.Rules.Term (checkExpr, isType_)
    import Agda.TypeChecking.Errors
    import Agda.TypeChecking.Warnings (runPM)

    import Agda.Syntax.Fixity
    import Agda.Syntax.Position
    import Agda.Syntax.Parser
    import Agda.Syntax.Common
    import Agda.Syntax.Concrete as C
    import Agda.Syntax.Concrete.Glyph
    import Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract.Pretty
    import Agda.Syntax.Info (mkDefInfo)
    import Agda.Syntax.Translation.ConcreteToAbstract
    import Agda.Syntax.Translation.AbstractToConcrete hiding (withScope)
    import Agda.Syntax.Scope.Base

    import Agda.Interaction.Base
    import Agda.Interaction.FindFile
    import Agda.Interaction.Options
    import Agda.Interaction.Options.Lenses as Lenses
    import Agda.Interaction.MakeCase
    import Agda.Interaction.SearchAbout
    import Agda.Interaction.Response hiding (Function, ExtendedLambda)
    import qualified Agda.Interaction.Response as R
    import qualified Agda.Interaction.BasicOps as B
    import Agda.Interaction.Highlighting.Precise hiding (Error, Postulate, singleton)
    import Agda.Interaction.Imports  ( Mode, pattern ScopeCheck, pattern TypeCheck )
    import qualified Agda.Interaction.Imports as Imp
    import Agda.Interaction.Highlighting.Generate

    import Agda.Compiler.Backend

    import Agda.Auto.Auto as Auto

    import Agda.Utils.Either
    import Agda.Utils.FileName
    import Agda.Utils.Function
    import Agda.Utils.Hash
    import Agda.Utils.Lens
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Pretty hiding (Mode)
    import Agda.Utils.Singleton
    import Agda.Utils.String
    import Agda.Utils.Time
    import Agda.Utils.Tuple

    import Agda.Utils.Impossible

    ------------------------------------------------------------------------
    -- The CommandM monad

    -- | Restore both 'TCState' and 'CommandState'.

    localStateCommandM :: CommandM a -> CommandM a
    localStateCommandM :: forall a. CommandM a -> CommandM a
    localStateCommandM CommandM a
    m = do
      CommandState
    cSt <- StateT CommandState TCM CommandState
    forall s (m :: * -> *). MonadState s m => m s
    get
      TCState
    tcSt <- StateT CommandState TCM TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
      a
    x <- CommandM a
    m
      TCState -> StateT CommandState TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    tcSt
      CommandState -> StateT CommandState TCM ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put CommandState
    cSt
      a -> CommandM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

    -- | Restore 'TCState', do not touch 'CommandState'.

    liftLocalState :: TCM a -> CommandM a
    liftLocalState :: forall a. TCM a -> CommandM a
    liftLocalState = TCMT IO a -> StateT CommandState TCM a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO a -> StateT CommandState TCM a)
    -> (TCMT IO a -> TCMT IO a)
    -> TCMT IO a
    -> StateT CommandState TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCMT IO a -> TCMT IO a
    forall a. TCM a -> TCM a
    localTCState

    -- | Build an opposite action to 'lift' for state monads.

    revLift
        :: MonadState st m
        => (forall c . m c -> st -> k (c, st))      -- ^ run
        -> (forall b . k b -> m b)                  -- ^ lift
        -> (forall x . (m a -> k x) -> k x) -> m a  -- ^ reverse lift in double negative position
    revLift :: forall st (m :: * -> *) (k :: * -> *) a.
    MonadState st m =>
    (forall c. m c -> st -> k (c, st))
    -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
    revLift forall c. m c -> st -> k (c, st)
    run forall b. k b -> m b
    lift' forall x. (m a -> k x) -> k x
    f = do
        st
    st <- m st
    forall s (m :: * -> *). MonadState s m => m s
    get
        (a
    a, st
    st') <- k (a, st) -> m (a, st)
    forall b. k b -> m b
    lift' (k (a, st) -> m (a, st)) -> k (a, st) -> m (a, st)
    forall a b. (a -> b) -> a -> b
    $ (m a -> k (a, st)) -> k (a, st)
    forall x. (m a -> k x) -> k x
    f (m a -> st -> k (a, st)
    forall c. m c -> st -> k (c, st)
    `run` st
    st)
        st -> m ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put st
    st'
        a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    revLiftTC
        :: MonadTCState m
        => (forall c . m c -> TCState -> k (c, TCState))  -- ^ run
        -> (forall b . k b -> m b)                        -- ^ lift
        -> (forall x . (m a -> k x) -> k x) -> m a        -- ^ reverse lift in double negative position
    revLiftTC :: forall (m :: * -> *) (k :: * -> *) a.
    MonadTCState m =>
    (forall c. m c -> TCState -> k (c, TCState))
    -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
    revLiftTC forall c. m c -> TCState -> k (c, TCState)
    run forall b. k b -> m b
    lift' forall x. (m a -> k x) -> k x
    f = do
        TCState
    st <- m TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
        (a
    a, TCState
    st') <- k (a, TCState) -> m (a, TCState)
    forall b. k b -> m b
    lift' (k (a, TCState) -> m (a, TCState))
    -> k (a, TCState) -> m (a, TCState)
    forall a b. (a -> b) -> a -> b
    $ (m a -> k (a, TCState)) -> k (a, TCState)
    forall x. (m a -> k x) -> k x
    f (m a -> TCState -> k (a, TCState)
    forall c. m c -> TCState -> k (c, TCState)
    `run` TCState
    st)
        TCState -> m ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    st'
        a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    -- | Opposite of 'liftIO' for 'CommandM'.
    --
    -- This function should only be applied to computations that are
    -- guaranteed not to raise any errors (except for 'IOException's).

    commandMToIO :: (forall x . (CommandM a -> IO x) -> IO x) -> CommandM a
    commandMToIO :: forall a. (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
    commandMToIO forall x. (CommandM a -> IO x) -> IO x
    ci_i = (forall c.
     StateT CommandState TCM c -> CommandState -> TCM (c, CommandState))
    -> (forall a. TCM a -> CommandM a)
    -> (forall x. (CommandM a -> TCM x) -> TCM x)
    -> CommandM a
    forall st (m :: * -> *) (k :: * -> *) a.
    MonadState st m =>
    (forall c. m c -> st -> k (c, st))
    -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
    revLift forall c.
    StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT forall a. TCM a -> CommandM a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ((forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a)
    -> (forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a
    forall a b. (a -> b) -> a -> b
    $ \CommandM a -> TCM x
    ct -> (forall c. TCM c -> TCState -> IO (c, TCState))
    -> (forall b. IO b -> TCM b)
    -> (forall x. (TCM x -> IO x) -> IO x)
    -> TCM x
    forall (m :: * -> *) (k :: * -> *) a.
    MonadTCState m =>
    (forall c. m c -> TCState -> k (c, TCState))
    -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
    revLiftTC forall c. TCM c -> TCState -> IO (c, TCState)
    runSafeTCM forall b. IO b -> TCM b
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ((forall x. (TCM x -> IO x) -> IO x) -> TCM x)
    -> (forall x. (TCM x -> IO x) -> IO x) -> TCM x
    forall a b. (a -> b) -> a -> b
    $ (CommandM a -> IO x) -> IO x
    forall x. (CommandM a -> IO x) -> IO x
    ci_i ((CommandM a -> IO x) -> IO x)
    -> ((TCM x -> IO x) -> CommandM a -> IO x)
    -> (TCM x -> IO x)
    -> IO x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((TCM x -> IO x) -> (CommandM a -> TCM x) -> CommandM a -> IO x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CommandM a -> TCM x
    ct)

    -- | Lift a TCM action transformer to a CommandM action transformer.

    liftCommandMT :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
    liftCommandMT :: forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    liftCommandMT forall a. TCM a -> TCM a
    f CommandM a
    m = (forall c.
     StateT CommandState TCM c -> CommandState -> TCM (c, CommandState))
    -> (forall a. TCM a -> CommandM a)
    -> (forall x. (CommandM a -> TCM x) -> TCM x)
    -> CommandM a
    forall st (m :: * -> *) (k :: * -> *) a.
    MonadState st m =>
    (forall c. m c -> st -> k (c, st))
    -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
    revLift forall c.
    StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT forall a. TCM a -> CommandM a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ((forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a)
    -> (forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a
    forall a b. (a -> b) -> a -> b
    $ TCM x -> TCM x
    forall a. TCM a -> TCM a
    f (TCM x -> TCM x)
    -> ((CommandM a -> TCM x) -> TCM x)
    -> (CommandM a -> TCM x)
    -> TCM x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((CommandM a -> TCM x) -> CommandM a -> TCM x
    forall a b. (a -> b) -> a -> b
    $ CommandM a
    m)

    -- | Ditto, but restore state.

    liftCommandMTLocalState :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
    liftCommandMTLocalState :: forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    liftCommandMTLocalState forall a. TCM a -> TCM a
    f = (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    liftCommandMT forall a. TCM a -> TCM a
    f (CommandM a -> CommandM a)
    -> (CommandM a -> CommandM a) -> CommandM a -> CommandM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CommandM a -> CommandM a
    forall a. CommandM a -> CommandM a
    localStateCommandM

    -- | Put a response by the callback function given by 'stInteractionOutputCallback'.

    putResponse :: Response -> CommandM ()
    putResponse :: Response -> StateT CommandState TCM ()
    putResponse = TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> (Response -> TCMT IO ())
    -> Response
    -> StateT CommandState TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Response -> TCMT IO ()
    appInteractionOutputCallback

    -- | A Lens for 'theInteractionPoints'.

    modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> CommandM ()
    modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> StateT CommandState TCM ()
    modifyTheInteractionPoints [InteractionId] -> [InteractionId]
    f = (CommandState -> CommandState) -> StateT CommandState TCM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
    -> (CommandState -> CommandState) -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ CommandState
    s ->
      CommandState
    s { theInteractionPoints :: [InteractionId]
    theInteractionPoints = [InteractionId] -> [InteractionId]
    f (CommandState -> [InteractionId]
    theInteractionPoints CommandState
    s) }

    -- * Operations for manipulating 'oldInteractionScopes'.

    -- | A Lens for 'oldInteractionScopes'.
    modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
    modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes)
    -> StateT CommandState TCM ()
    modifyOldInteractionScopes OldInteractionScopes -> OldInteractionScopes
    f = (CommandState -> CommandState) -> StateT CommandState TCM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
    -> (CommandState -> CommandState) -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ CommandState
    s ->
      CommandState
    s { oldInteractionScopes :: OldInteractionScopes
    oldInteractionScopes = OldInteractionScopes -> OldInteractionScopes
    f (OldInteractionScopes -> OldInteractionScopes)
    -> OldInteractionScopes -> OldInteractionScopes
    forall a b. (a -> b) -> a -> b
    $ CommandState -> OldInteractionScopes
    oldInteractionScopes CommandState
    s }

    insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()
    insertOldInteractionScope :: InteractionId -> ScopeInfo -> StateT CommandState TCM ()
    insertOldInteractionScope InteractionId
    ii ScopeInfo
    scope = do
      TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "interaction.scope" Int
    20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "inserting old interaction scope " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ InteractionId -> [Char]
    forall a. Show a => a -> [Char]
    show InteractionId
    ii
      (OldInteractionScopes -> OldInteractionScopes)
    -> StateT CommandState TCM ()
    modifyOldInteractionScopes ((OldInteractionScopes -> OldInteractionScopes)
     -> StateT CommandState TCM ())
    -> (OldInteractionScopes -> OldInteractionScopes)
    -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId
    -> ScopeInfo -> OldInteractionScopes -> OldInteractionScopes
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert InteractionId
    ii ScopeInfo
    scope

    removeOldInteractionScope :: InteractionId -> CommandM ()
    removeOldInteractionScope :: InteractionId -> StateT CommandState TCM ()
    removeOldInteractionScope InteractionId
    ii = do
      TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "interaction.scope" Int
    20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "removing old interaction scope " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ InteractionId -> [Char]
    forall a. Show a => a -> [Char]
    show InteractionId
    ii
      (OldInteractionScopes -> OldInteractionScopes)
    -> StateT CommandState TCM ()
    modifyOldInteractionScopes ((OldInteractionScopes -> OldInteractionScopes)
     -> StateT CommandState TCM ())
    -> (OldInteractionScopes -> OldInteractionScopes)
    -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> OldInteractionScopes -> OldInteractionScopes
    forall k a. Ord k => k -> Map k a -> Map k a
    Map.delete InteractionId
    ii

    getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
    getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
    getOldInteractionScope InteractionId
    ii = do
      Maybe ScopeInfo
    ms <- (CommandState -> Maybe ScopeInfo)
    -> StateT CommandState TCM (Maybe ScopeInfo)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ((CommandState -> Maybe ScopeInfo)
     -> StateT CommandState TCM (Maybe ScopeInfo))
    -> (CommandState -> Maybe ScopeInfo)
    -> StateT CommandState TCM (Maybe ScopeInfo)
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> OldInteractionScopes -> Maybe ScopeInfo
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup InteractionId
    ii (OldInteractionScopes -> Maybe ScopeInfo)
    -> (CommandState -> OldInteractionScopes)
    -> CommandState
    -> Maybe ScopeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CommandState -> OldInteractionScopes
    oldInteractionScopes
      case Maybe ScopeInfo
    ms of
        Maybe ScopeInfo
    Nothing    -> [Char] -> CommandM ScopeInfo
    forall (m :: * -> *) a. MonadFail m => [Char] -> m a
    fail ([Char] -> CommandM ScopeInfo) -> [Char] -> CommandM ScopeInfo
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "not an old interaction point: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ InteractionId -> [Char]
    forall a. Show a => a -> [Char]
    show InteractionId
    ii
        Just ScopeInfo
    scope -> ScopeInfo -> CommandM ScopeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return ScopeInfo
    scope

    -- | Do setup and error handling for a command.

    handleCommand_ :: CommandM () -> CommandM ()
    handleCommand_ :: StateT CommandState TCM () -> StateT CommandState TCM ()
    handleCommand_ = (forall a. CommandM a -> CommandM a)
    -> StateT CommandState TCM ()
    -> StateT CommandState TCM ()
    -> StateT CommandState TCM ()
    handleCommand forall a. a -> a
    forall a. CommandM a -> CommandM a
    id (() -> StateT CommandState TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

    handleCommand :: (forall a. CommandM a -> CommandM a) -> CommandM () -> CommandM () -> CommandM ()
    handleCommand :: (forall a. CommandM a -> CommandM a)
    -> StateT CommandState TCM ()
    -> StateT CommandState TCM ()
    -> StateT CommandState TCM ()
    handleCommand forall a. CommandM a -> CommandM a
    wrap StateT CommandState TCM ()
    onFail StateT CommandState TCM ()
    cmd = StateT CommandState TCM () -> StateT CommandState TCM ()
    handleNastyErrors (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a. CommandM a -> CommandM a
    wrap (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        TCState
    oldState <- StateT CommandState TCM TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC

        -- -- Andreas, 2016-11-18 OLD CODE:
        -- -- onFail and handleErr are executed in "new" command state (not TCState).
        -- -- But it seems that if an exception is raised, it is identical to the old state,
        -- -- see code for catchErr.
        -- res <- (`catchErr` (return . Just)) $ Nothing <$ cmd
        -- maybe (return ()) (\ e -> onFail >> handleErr e) res

        -- Andreas, 2016-11-18 NEW CODE: execute onFail and handleErr in handler
        -- which means (looking at catchErr) they run in state s rathern than s'.
        -- Yet, it looks like s == s' in case the command failed.
        StateT CommandState TCM ()
    cmd StateT CommandState TCM ()
    -> (TCErr -> StateT CommandState TCM ())
    -> StateT CommandState TCM ()
    forall a. CommandM a -> (TCErr -> CommandM a) -> CommandM a
    `catchErr` \ TCErr
    e -> do
          StateT CommandState TCM ()
    onFail
          Maybe HighlightingMethod -> TCErr -> StateT CommandState TCM ()
    handleErr Maybe HighlightingMethod
    forall a. Maybe a
    Nothing TCErr
    e
          -- Andreas, 2016-11-18, issue #2174
          -- Reset TCState after error is handled, to get rid of metas created during failed command
          TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            PersistentTCState
    newPersistentState <- Lens' PersistentTCState TCState -> TCM PersistentTCState
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' PersistentTCState TCState
    lensPersistentState
            TCState -> TCMT IO ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    oldState
            Lens' PersistentTCState TCState
    lensPersistentState Lens' PersistentTCState TCState -> PersistentTCState -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` PersistentTCState
    newPersistentState

      where
        -- Preserves state so we can do unsolved meta highlighting
        catchErr :: CommandM a -> (TCErr -> CommandM a) -> CommandM a
        catchErr :: forall a. CommandM a -> (TCErr -> CommandM a) -> CommandM a
    catchErr CommandM a
    m TCErr -> CommandM a
    h = do
          CommandState
    s       <- StateT CommandState TCM CommandState
    forall s (m :: * -> *). MonadState s m => m s
    get
          (a
    x, CommandState
    s') <- TCMT IO (a, CommandState)
    -> StateT CommandState TCM (a, CommandState)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO (a, CommandState)
     -> StateT CommandState TCM (a, CommandState))
    -> TCMT IO (a, CommandState)
    -> StateT CommandState TCM (a, CommandState)
    forall a b. (a -> b) -> a -> b
    $ do CommandM a -> CommandState -> TCMT IO (a, CommandState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT CommandM a
    m CommandState
    s
             TCMT IO (a, CommandState)
    -> (TCErr -> TCMT IO (a, CommandState))
    -> TCMT IO (a, CommandState)
    forall a. TCM a -> (TCErr -> TCM a) -> TCM a
    `catchError_` \ TCErr
    e ->
               CommandM a -> CommandState -> TCMT IO (a, CommandState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (TCErr -> CommandM a
    h TCErr
    e) CommandState
    s
          CommandState -> StateT CommandState TCM ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put CommandState
    s'
          a -> CommandM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

        -- Handle every possible kind of error (#637), except for
        -- AsyncCancelled, which is used to abort Agda.
        handleNastyErrors :: CommandM () -> CommandM ()
        handleNastyErrors :: StateT CommandState TCM () -> StateT CommandState TCM ()
    handleNastyErrors StateT CommandState TCM ()
    m = (forall x. (StateT CommandState TCM () -> IO x) -> IO x)
    -> StateT CommandState TCM ()
    forall a. (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
    commandMToIO ((forall x. (StateT CommandState TCM () -> IO x) -> IO x)
     -> StateT CommandState TCM ())
    -> (forall x. (StateT CommandState TCM () -> IO x) -> IO x)
    -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ StateT CommandState TCM () -> IO x
    toIO -> do
          let handle :: SomeException -> IO (Either AsyncCancelled x)
    handle SomeException
    e =
                x -> Either AsyncCancelled x
    forall a b. b -> Either a b
    Right (x -> Either AsyncCancelled x)
    -> IO x -> IO (Either AsyncCancelled x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                  StateT CommandState TCM () -> IO x
    toIO (Maybe HighlightingMethod -> TCErr -> StateT CommandState TCM ()
    handleErr (HighlightingMethod -> Maybe HighlightingMethod
    forall a. a -> Maybe a
    Just HighlightingMethod
    Direct) (TCErr -> StateT CommandState TCM ())
    -> TCErr -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $
                            Range -> Doc -> TCErr
    Exception Range
    forall a. Range' a
    noRange (Doc -> TCErr) -> Doc -> TCErr
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ SomeException -> [Char]
    forall a. Show a => a -> [Char]
    show SomeException
    e)

              asyncHandler :: AsyncCancelled -> m (Either AsyncCancelled b)
    asyncHandler e :: AsyncCancelled
    e@AsyncCancelled
    AsyncCancelled = Either AsyncCancelled b -> m (Either AsyncCancelled b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AsyncCancelled -> Either AsyncCancelled b
    forall a b. a -> Either a b
    Left AsyncCancelled
    e)

              generalHandler :: SomeException -> IO (Either AsyncCancelled x)
    generalHandler (SomeException
    e :: E.SomeException) = SomeException -> IO (Either AsyncCancelled x)
    handle SomeException
    e

          Either AsyncCancelled x
    r <- ((x -> Either AsyncCancelled x
    forall a b. b -> Either a b
    Right (x -> Either AsyncCancelled x)
    -> IO x -> IO (Either AsyncCancelled x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> StateT CommandState TCM () -> IO x
    toIO StateT CommandState TCM ()
    m) IO (Either AsyncCancelled x)
    -> (AsyncCancelled -> IO (Either AsyncCancelled x))
    -> IO (Either AsyncCancelled x)
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `E.catch` AsyncCancelled -> IO (Either AsyncCancelled x)
    forall {m :: * -> *} {b}.
    Monad m =>
    AsyncCancelled -> m (Either AsyncCancelled b)
    asyncHandler)
                 IO (Either AsyncCancelled x)
    -> (SomeException -> IO (Either AsyncCancelled x))
    -> IO (Either AsyncCancelled x)
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `E.catch` SomeException -> IO (Either AsyncCancelled x)
    generalHandler
          case Either AsyncCancelled x
    r of
            Right x
    x -> x -> IO x
    forall (m :: * -> *) a. Monad m => a -> m a
    return x
    x
            Left AsyncCancelled
    e  -> AsyncCancelled -> IO x
    forall e a. Exception e => e -> IO a
    E.throwIO AsyncCancelled
    e

        -- Displays an error and instructs Emacs to jump to the site of the
        -- error. Because this function may switch the focus to another file
        -- the status information is also updated.
        handleErr :: Maybe HighlightingMethod -> TCErr -> StateT CommandState TCM ()
    handleErr Maybe HighlightingMethod
    method TCErr
    e = do
            HighlightingInfoBuilder
    unsolved <- TCMT IO HighlightingInfoBuilder
    -> StateT CommandState TCM HighlightingInfoBuilder
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO HighlightingInfoBuilder
     -> StateT CommandState TCM HighlightingInfoBuilder)
    -> TCMT IO HighlightingInfoBuilder
    -> StateT CommandState TCM HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ TCMT IO HighlightingInfoBuilder
    computeUnsolvedInfo
            HighlightingInfoBuilder
    err     <- TCMT IO HighlightingInfoBuilder
    -> StateT CommandState TCM HighlightingInfoBuilder
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO HighlightingInfoBuilder
     -> StateT CommandState TCM HighlightingInfoBuilder)
    -> TCMT IO HighlightingInfoBuilder
    -> StateT CommandState TCM HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ TCErr -> TCMT IO HighlightingInfoBuilder
    errorHighlighting TCErr
    e
            ModuleToSource
    modFile <- TCMT IO ModuleToSource -> StateT CommandState TCM ModuleToSource
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO ModuleToSource -> StateT CommandState TCM ModuleToSource)
    -> TCMT IO ModuleToSource -> StateT CommandState TCM ModuleToSource
    forall a b. (a -> b) -> a -> b
    $ Lens' ModuleToSource TCState -> TCMT IO ModuleToSource
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' ModuleToSource TCState
    stModuleToSource
            HighlightingMethod
    method  <- case Maybe HighlightingMethod
    method of
              Maybe HighlightingMethod
    Nothing -> TCMT IO HighlightingMethod
    -> StateT CommandState TCM HighlightingMethod
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO HighlightingMethod
     -> StateT CommandState TCM HighlightingMethod)
    -> TCMT IO HighlightingMethod
    -> StateT CommandState TCM HighlightingMethod
    forall a b. (a -> b) -> a -> b
    $ Lens' HighlightingMethod TCEnv -> TCMT IO HighlightingMethod
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' HighlightingMethod TCEnv
    eHighlightingMethod
              Just HighlightingMethod
    m  -> HighlightingMethod -> StateT CommandState TCM HighlightingMethod
    forall (m :: * -> *) a. Monad m => a -> m a
    return HighlightingMethod
    m
            let info :: HighlightingInfo
    info = HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert (HighlightingInfoBuilder -> HighlightingInfo)
    -> HighlightingInfoBuilder -> HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $ HighlightingInfoBuilder
    err HighlightingInfoBuilder
    -> HighlightingInfoBuilder -> HighlightingInfoBuilder
    forall a. Semigroup a => a -> a -> a
    <> HighlightingInfoBuilder
    unsolved
                         -- Errors take precedence over unsolved things.

            -- TODO: make a better predicate for this
            Bool
    noError <- TCMT IO Bool -> StateT CommandState TCM Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Bool -> StateT CommandState TCM Bool)
    -> TCMT IO Bool -> StateT CommandState TCM Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Bool
    forall a. Null a => a -> Bool
    null ([Char] -> Bool) -> TCMT IO [Char] -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCErr -> TCMT IO [Char]
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
    prettyError TCErr
    e

            Bool
    showImpl <- TCMT IO Bool -> StateT CommandState TCM Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Bool -> StateT CommandState TCM Bool)
    -> TCMT IO Bool -> StateT CommandState TCM Bool
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> Bool
    optShowImplicit (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' PragmaOptions TCState
    stPragmaOptions
            Bool
    showIrr <- TCMT IO Bool -> StateT CommandState TCM Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Bool -> StateT CommandState TCM Bool)
    -> TCMT IO Bool -> StateT CommandState TCM Bool
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> Bool
    optShowIrrelevant (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' PragmaOptions TCState
    stPragmaOptions
            Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    noError (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Response -> StateT CommandState TCM ())
    -> [Response] -> StateT CommandState TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Response -> StateT CommandState TCM ()
    putResponse ([Response] -> StateT CommandState TCM ())
    -> [Response] -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $
                [ DisplayInfo -> Response
    Resp_DisplayInfo (DisplayInfo -> Response) -> DisplayInfo -> Response
    forall a b. (a -> b) -> a -> b
    $ Info_Error -> DisplayInfo
    Info_Error (Info_Error -> DisplayInfo) -> Info_Error -> DisplayInfo
    forall a b. (a -> b) -> a -> b
    $ TCErr -> Info_Error
    Info_GenericError TCErr
    e ] [Response] -> [Response] -> [Response]
    forall a. [a] -> [a] -> [a]
    ++
                Range -> [Response]
    tellEmacsToJumpToError (TCErr -> Range
    forall a. HasRange a => a -> Range
    getRange TCErr
    e) [Response] -> [Response] -> [Response]
    forall a. [a] -> [a] -> [a]
    ++
                [ HighlightingInfo
    -> RemoveTokenBasedHighlighting
    -> HighlightingMethod
    -> ModuleToSource
    -> Response
    Resp_HighlightingInfo HighlightingInfo
    info RemoveTokenBasedHighlighting
    KeepHighlighting
                                        HighlightingMethod
    method ModuleToSource
    modFile ] [Response] -> [Response] -> [Response]
    forall a. [a] -> [a] -> [a]
    ++
                [ Status -> Response
    Resp_Status (Status -> Response) -> Status -> Response
    forall a b. (a -> b) -> a -> b
    $ Status :: Bool -> Bool -> Bool -> Status
    Status { sChecked :: Bool
    sChecked = Bool
    False
                                       , sShowImplicitArguments :: Bool
    sShowImplicitArguments = Bool
    showImpl
                                       , sShowIrrelevantArguments :: Bool
    sShowIrrelevantArguments = Bool
    showIrr
                                       } ]

    -- | Run an 'IOTCM' value, catch the exceptions, emit output
    --
    --   If an error happens the state of 'CommandM' does not change,
    --   but stPersistent may change (which contains successfully
    --   loaded interfaces for example).

    runInteraction :: IOTCM -> CommandM ()
    runInteraction :: IOTCM -> StateT CommandState TCM ()
    runInteraction (IOTCM [Char]
    current HighlightingLevel
    highlighting HighlightingMethod
    highlightingMethod Interaction' Range
    cmd) =
      (forall a. CommandM a -> CommandM a)
    -> StateT CommandState TCM ()
    -> StateT CommandState TCM ()
    -> StateT CommandState TCM ()
    handleCommand forall a. CommandM a -> CommandM a
    inEmacs StateT CommandState TCM ()
    onFail (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        AbsolutePath
    currentAbs <- IO AbsolutePath -> StateT CommandState TCM AbsolutePath
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO AbsolutePath -> StateT CommandState TCM AbsolutePath)
    -> IO AbsolutePath -> StateT CommandState TCM AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO AbsolutePath
    absolute [Char]
    current
        -- Raises an error if the given file is not the one currently
        -- loaded.
        Maybe CurrentFile
    cf <- (CommandState -> Maybe CurrentFile)
    -> StateT CommandState TCM (Maybe CurrentFile)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets CommandState -> Maybe CurrentFile
    theCurrentFile
        Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Bool -> Bool
    not (Interaction' Range -> Bool
    independent Interaction' Range
    cmd) Bool -> Bool -> Bool
    && AbsolutePath -> Maybe AbsolutePath
    forall a. a -> Maybe a
    Just AbsolutePath
    currentAbs Maybe AbsolutePath -> Maybe AbsolutePath -> Bool
    forall a. Eq a => a -> a -> Bool
    /= (CurrentFile -> AbsolutePath
    currentFilePath (CurrentFile -> AbsolutePath)
    -> Maybe CurrentFile -> Maybe AbsolutePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe CurrentFile
    cf)) (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            let mode :: Mode
    mode = Mode
    TypeCheck
            [Char]
    -> [[Char]]
    -> Bool
    -> Mode
    -> (CheckResult -> StateT CommandState TCM ())
    -> StateT CommandState TCM ()
    forall a.
    [Char]
    -> [[Char]]
    -> Bool
    -> Mode
    -> (CheckResult -> CommandM a)
    -> CommandM a
    cmd_load' [Char]
    current [] Bool
    True Mode
    mode ((CheckResult -> StateT CommandState TCM ())
     -> StateT CommandState TCM ())
    -> (CheckResult -> StateT CommandState TCM ())
    -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ \CheckResult
    _ -> () -> StateT CommandState TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

        StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a. CommandM a -> CommandM a
    withCurrentFile (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ Interaction' Range -> StateT CommandState TCM ()
    interpret Interaction' Range
    cmd

        Maybe CurrentFile
    cf' <- (CommandState -> Maybe CurrentFile)
    -> StateT CommandState TCM (Maybe CurrentFile)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets CommandState -> Maybe CurrentFile
    theCurrentFile
        Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Interaction' Range -> Bool
    updateInteractionPointsAfter Interaction' Range
    cmd
                Bool -> Bool -> Bool
    &&
              AbsolutePath -> Maybe AbsolutePath
    forall a. a -> Maybe a
    Just AbsolutePath
    currentAbs Maybe AbsolutePath -> Maybe AbsolutePath -> Bool
    forall a. Eq a => a -> a -> Bool
    == (CurrentFile -> AbsolutePath
    currentFilePath (CurrentFile -> AbsolutePath)
    -> Maybe CurrentFile -> Maybe AbsolutePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe CurrentFile
    cf')) (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            Response -> StateT CommandState TCM ()
    putResponse (Response -> StateT CommandState TCM ())
    -> ([InteractionId] -> Response)
    -> [InteractionId]
    -> StateT CommandState TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [InteractionId] -> Response
    Resp_InteractionPoints ([InteractionId] -> StateT CommandState TCM ())
    -> StateT CommandState TCM [InteractionId]
    -> StateT CommandState TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (CommandState -> [InteractionId])
    -> StateT CommandState TCM [InteractionId]
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets CommandState -> [InteractionId]
    theInteractionPoints

      where
        inEmacs :: forall a. CommandM a -> CommandM a
        inEmacs :: forall a. CommandM a -> CommandM a
    inEmacs = (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    liftCommandMT ((forall a. TCM a -> TCM a) -> CommandM a -> CommandM a)
    -> (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    forall a b. (a -> b) -> a -> b
    $ TCEnv -> TCMT IO x -> TCMT IO x
    forall (m :: * -> *) a. MonadTCEnv m => TCEnv -> m a -> m a
    withEnv (TCEnv -> TCMT IO x -> TCMT IO x)
    -> TCEnv -> TCMT IO x -> TCMT IO x
    forall a b. (a -> b) -> a -> b
    $ TCEnv
    initEnv
                { envHighlightingLevel :: HighlightingLevel
    envHighlightingLevel  = HighlightingLevel
    highlighting
                , envHighlightingMethod :: HighlightingMethod
    envHighlightingMethod = HighlightingMethod
    highlightingMethod
                }

        -- If an independent command fails we should reset theCurrentFile (Issue853).
        onFail :: StateT CommandState TCM ()
    onFail | Interaction' Range -> Bool
    independent Interaction' Range
    cmd = (CommandState -> CommandState) -> StateT CommandState TCM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
    -> (CommandState -> CommandState) -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ CommandState
    s -> CommandState
    s { theCurrentFile :: Maybe CurrentFile
    theCurrentFile = Maybe CurrentFile
    forall a. Maybe a
    Nothing }
               | Bool
    otherwise       = () -> StateT CommandState TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    ------------------------------------------------------------------------
    -- Command queues

    -- | If the next command from the command queue is anything but an
    -- actual command, then the command is returned.
    --
    -- If the command is an 'IOTCM' command, then the following happens:
    -- The given computation is applied to the command and executed. If an
    -- abort command is encountered (and acted upon), then the computation
    -- is interrupted, the persistent state and all options are restored,
    -- and some commands are sent to the frontend. If the computation was
    -- not interrupted, then its result is returned.

    -- TODO: It might be nice if some of the changes to the persistent
    -- state inflicted by the interrupted computation were preserved.

    maybeAbort :: (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
    maybeAbort :: forall a. (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
    maybeAbort IOTCM -> CommandM a
    m = do
      CommandState
    commandState <- StateT CommandState TCM CommandState
    forall s (m :: * -> *). MonadState s m => m s
    get
      let q :: CommandQueue
    q = CommandState -> CommandQueue
    commandQueue CommandState
    commandState
      (Integer
    n, Command
    cmd) <- IO (Integer, Command) -> StateT CommandState TCM (Integer, Command)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Integer, Command)
     -> StateT CommandState TCM (Integer, Command))
    -> IO (Integer, Command)
    -> StateT CommandState TCM (Integer, Command)
    forall a b. (a -> b) -> a -> b
    $ STM (Integer, Command) -> IO (Integer, Command)
    forall a. STM a -> IO a
    atomically (STM (Integer, Command) -> IO (Integer, Command))
    -> STM (Integer, Command) -> IO (Integer, Command)
    forall a b. (a -> b) -> a -> b
    $ TChan (Integer, Command) -> STM (Integer, Command)
    forall a. TChan a -> STM a
    readTChan (CommandQueue -> TChan (Integer, Command)
    commands CommandQueue
    q)
      case Command
    cmd of
        Command
    Done      -> Command' (Maybe a) -> CommandM (Command' (Maybe a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Command' (Maybe a)
    forall a. Command' a
    Done
        Error [Char]
    e   -> Command' (Maybe a) -> CommandM (Command' (Maybe a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> Command' (Maybe a)
    forall a. [Char] -> Command' a
    Error [Char]
    e)
        Command IOTCM
    c -> do
          TCState
    tcState <- StateT CommandState TCM TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
          TCEnv
    tcEnv   <- StateT CommandState TCM TCEnv
    forall (m :: * -> *). MonadTCEnv m => m TCEnv
    askTC
          Either ((a, CommandState), TCState) Integer
    result  <- IO (Either ((a, CommandState), TCState) Integer)
    -> StateT
         CommandState TCM (Either ((a, CommandState), TCState) Integer)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either ((a, CommandState), TCState) Integer)
     -> StateT
          CommandState TCM (Either ((a, CommandState), TCState) Integer))
    -> IO (Either ((a, CommandState), TCState) Integer)
    -> StateT
         CommandState TCM (Either ((a, CommandState), TCState) Integer)
    forall a b. (a -> b) -> a -> b
    $ IO ((a, CommandState), TCState)
    -> IO Integer -> IO (Either ((a, CommandState), TCState) Integer)
    forall a b. IO a -> IO b -> IO (Either a b)
    race
                       (TCEnv
    -> TCState
    -> TCMT IO (a, CommandState)
    -> IO ((a, CommandState), TCState)
    forall (m :: * -> *) a.
    MonadIO m =>
    TCEnv -> TCState -> TCMT m a -> m (a, TCState)
    runTCM TCEnv
    tcEnv TCState
    tcState (TCMT IO (a, CommandState) -> IO ((a, CommandState), TCState))
    -> TCMT IO (a, CommandState) -> IO ((a, CommandState), TCState)
    forall a b. (a -> b) -> a -> b
    $ CommandM a -> CommandState -> TCMT IO (a, CommandState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (IOTCM -> CommandM a
    m IOTCM
    c) CommandState
    commandState)
                       (Integer -> CommandQueue -> IO Integer
    waitForAbort Integer
    n CommandQueue
    q)
          case Either ((a, CommandState), TCState) Integer
    result of
            Left ((a
    x, CommandState
    commandState'), TCState
    tcState') -> do
              TCState -> StateT CommandState TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    tcState'
              CommandState -> StateT CommandState TCM ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put CommandState
    commandState'
              case IOTCM
    c of
                IOTCM [Char]
    _ HighlightingLevel
    _ HighlightingMethod
    _ Interaction' Range
    Cmd_exit -> do
                  Response -> StateT CommandState TCM ()
    putResponse Response
    Resp_DoneExiting
                  Command' (Maybe a) -> CommandM (Command' (Maybe a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Command' (Maybe a)
    forall a. Command' a
    Done
                IOTCM
    _ -> Command' (Maybe a) -> CommandM (Command' (Maybe a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> Command' (Maybe a)
    forall a. a -> Command' a
    Command (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x))
            Right Integer
    a -> do
              IO () -> StateT CommandState TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> StateT CommandState TCM ())
    -> IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ CommandQueue -> Integer -> IO ()
    popAbortedCommands CommandQueue
    q Integer
    a
              TCState -> StateT CommandState TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC (TCState -> StateT CommandState TCM ())
    -> TCState -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCState
    initState
                { stPersistentState :: PersistentTCState
    stPersistentState = TCState -> PersistentTCState
    stPersistentState TCState
    tcState
                , stPreScopeState :: PreScopeState
    stPreScopeState   =
                    (TCState -> PreScopeState
    stPreScopeState TCState
    initState)
                      { stPrePragmaOptions :: PragmaOptions
    stPrePragmaOptions =
                          PreScopeState -> PragmaOptions
    stPrePragmaOptions
                            (TCState -> PreScopeState
    stPreScopeState TCState
    tcState)
                      }
                }
              CommandState -> StateT CommandState TCM ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (CommandState -> StateT CommandState TCM ())
    -> CommandState -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ (CommandQueue -> CommandState
    initCommandState (CommandState -> CommandQueue
    commandQueue CommandState
    commandState))
                { optionsOnReload :: CommandLineOptions
    optionsOnReload = CommandState -> CommandLineOptions
    optionsOnReload CommandState
    commandState
                }
              Response -> StateT CommandState TCM ()
    putResponse Response
    Resp_DoneAborting
              StateT CommandState TCM ()
    displayStatus
              Command' (Maybe a) -> CommandM (Command' (Maybe a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> Command' (Maybe a)
    forall a. a -> Command' a
    Command Maybe a
    forall a. Maybe a
    Nothing)
      where

      -- Returns if the currently executing command should be aborted.
      -- The "abort number" is returned.

      waitForAbort
        :: Integer       -- The number of the currently executing command.
        -> CommandQueue  -- The command queue.
        -> IO Integer
      waitForAbort :: Integer -> CommandQueue -> IO Integer
    waitForAbort Integer
    n CommandQueue
    q = do
        STM Integer -> IO Integer
    forall a. STM a -> IO a
    atomically (STM Integer -> IO Integer) -> STM Integer -> IO Integer
    forall a b. (a -> b) -> a -> b
    $ do
          Maybe Integer
    a <- TVar (Maybe Integer) -> STM (Maybe Integer)
    forall a. TVar a -> STM a
    readTVar (CommandQueue -> TVar (Maybe Integer)
    abort CommandQueue
    q)
          case Maybe Integer
    a of
            Just Integer
    a' | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    a' -> Integer -> STM Integer
    forall (m :: * -> *) a. Monad m => a -> m a
    return Integer
    a'
            Maybe Integer
    _                 -> STM Integer
    forall a. STM a
    retry

      -- Removes every command for which the command number is at most
      -- the given number (the "abort number") from the command queue.
      --
      -- New commands could be added to the end of the queue while this
      -- computation is running. This does not lead to a race condition,
      -- because those commands have higher command numbers, so they will
      -- not be removed.

      popAbortedCommands :: CommandQueue -> Integer -> IO ()
      popAbortedCommands :: CommandQueue -> Integer -> IO ()
    popAbortedCommands CommandQueue
    q Integer
    n = do
        Bool
    done <- STM Bool -> IO Bool
    forall a. STM a -> IO a
    atomically (STM Bool -> IO Bool) -> STM Bool -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ do
          Maybe (Integer, Command)
    cmd <- TChan (Integer, Command) -> STM (Maybe (Integer, Command))
    forall a. TChan a -> STM (Maybe a)
    tryReadTChan (CommandQueue -> TChan (Integer, Command)
    commands CommandQueue
    q)
          case Maybe (Integer, Command)
    cmd of
            Maybe (Integer, Command)
    Nothing -> Bool -> STM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
            Just (Integer, Command)
    c  ->
              if (Integer, Command) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Command)
    c Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    n then
                Bool -> STM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
               else do
                TChan (Integer, Command) -> (Integer, Command) -> STM ()
    forall a. TChan a -> a -> STM ()
    unGetTChan (CommandQueue -> TChan (Integer, Command)
    commands CommandQueue
    q) (Integer, Command)
    c
                Bool -> STM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    done (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
          CommandQueue -> Integer -> IO ()
    popAbortedCommands CommandQueue
    q Integer
    n

    -- | Creates a command queue, and forks a thread that writes commands
    -- to the queue. The queue is returned.

    initialiseCommandQueue
      :: IO Command
         -- ^ Returns the next command.
      -> IO CommandQueue
    initialiseCommandQueue :: IO Command -> IO CommandQueue
    initialiseCommandQueue IO Command
    next = do
      TChan (Integer, Command)
    commands <- IO (TChan (Integer, Command))
    forall a. IO (TChan a)
    newTChanIO
      TVar (Maybe Integer)
    abort    <- Maybe Integer -> IO (TVar (Maybe Integer))
    forall a. a -> IO (TVar a)
    newTVarIO Maybe Integer
    forall a. Maybe a
    Nothing

      let -- Read commands. The argument is the number of the previous
          -- command (other than abort commands) that was read, if any.
          readCommands :: Integer -> IO ()
    readCommands Integer
    n = do
            Command
    c <- IO Command
    next
            case Command
    c of
              Command (IOTCM [Char]
    _ HighlightingLevel
    _ HighlightingMethod
    _ Interaction' Range
    Cmd_abort) -> do
                STM () -> IO ()
    forall a. STM a -> IO a
    atomically (STM () -> IO ()) -> STM () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ TVar (Maybe Integer) -> Maybe Integer -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (Maybe Integer)
    abort (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    n)
                Integer -> IO ()
    readCommands Integer
    n
              Command
    _ -> do
                let n' :: Integer
    n' = (Integer -> Integer
    forall a. Enum a => a -> a
    succ Integer
    n)
                STM () -> IO ()
    forall a. STM a -> IO a
    atomically (STM () -> IO ()) -> STM () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ TChan (Integer, Command) -> (Integer, Command) -> STM ()
    forall a. TChan a -> a -> STM ()
    writeTChan TChan (Integer, Command)
    commands (Integer
    n', Command
    c)
                case Command
    c of
                  Command
    Done -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                  Command
    _    -> Integer -> IO ()
    readCommands Integer
    n'

      ThreadId
    _ <- IO () -> IO ThreadId
    forkIO (Integer -> IO ()
    readCommands Integer
    0)

      CommandQueue -> IO CommandQueue
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CommandQueue :: TChan (Integer, Command) -> TVar (Maybe Integer) -> CommandQueue
    CommandQueue { TVar (Maybe Integer)
    TChan (Integer, Command)
    abort :: TVar (Maybe Integer)
    commands :: TChan (Integer, Command)
    abort :: TVar (Maybe Integer)
    commands :: TChan (Integer, Command)
    .. })

    ---------------------------------------------------------

    -- | Can the command run even if the relevant file has not been loaded
    --   into the state?

    independent :: Interaction -> Bool
    independent :: Interaction' Range -> Bool
    independent (Cmd_load {})                   = Bool
    True
    independent (Cmd_compile {})                = Bool
    True
    independent (Cmd_load_highlighting_info {}) = Bool
    True
    independent Cmd_tokenHighlighting {}        = Bool
    True
    independent Interaction' Range
    Cmd_show_version                = Bool
    True
    independent Interaction' Range
    _                               = Bool
    False

    -- | Should 'Resp_InteractionPoints' be issued after the command has
    -- run?

    updateInteractionPointsAfter :: Interaction -> Bool
    updateInteractionPointsAfter :: Interaction' Range -> Bool
    updateInteractionPointsAfter Cmd_load{}                          = Bool
    True
    updateInteractionPointsAfter Cmd_compile{}                       = Bool
    True
    updateInteractionPointsAfter Cmd_constraints{}                   = Bool
    False
    updateInteractionPointsAfter Cmd_metas{}                         = Bool
    False
    updateInteractionPointsAfter Cmd_show_module_contents_toplevel{} = Bool
    False
    updateInteractionPointsAfter Cmd_search_about_toplevel{}         = Bool
    False
    updateInteractionPointsAfter Cmd_solveAll{}                      = Bool
    True
    updateInteractionPointsAfter Cmd_solveOne{}                      = Bool
    True
    updateInteractionPointsAfter Cmd_infer_toplevel{}                = Bool
    False
    updateInteractionPointsAfter Cmd_compute_toplevel{}              = Bool
    False
    updateInteractionPointsAfter Cmd_load_highlighting_info{}        = Bool
    False
    updateInteractionPointsAfter Cmd_tokenHighlighting{}             = Bool
    False
    updateInteractionPointsAfter Cmd_highlight{}                     = Bool
    True
    updateInteractionPointsAfter ShowImplicitArgs{}                  = Bool
    False
    updateInteractionPointsAfter ToggleImplicitArgs{}                = Bool
    False
    updateInteractionPointsAfter ShowIrrelevantArgs{}                = Bool
    False
    updateInteractionPointsAfter ToggleIrrelevantArgs{}              = Bool
    False
    updateInteractionPointsAfter Cmd_give{}                          = Bool
    True
    updateInteractionPointsAfter Cmd_refine{}                        = Bool
    True
    updateInteractionPointsAfter Cmd_intro{}                         = Bool
    True
    updateInteractionPointsAfter Cmd_refine_or_intro{}               = Bool
    True
    updateInteractionPointsAfter Cmd_autoOne{}                       = Bool
    True
    updateInteractionPointsAfter Cmd_autoAll{}                       = Bool
    True
    updateInteractionPointsAfter Cmd_context{}                       = Bool
    False
    updateInteractionPointsAfter Cmd_helper_function{}               = Bool
    False
    updateInteractionPointsAfter Cmd_infer{}                         = Bool
    False
    updateInteractionPointsAfter Cmd_goal_type{}                     = Bool
    False
    updateInteractionPointsAfter Cmd_elaborate_give{}                = Bool
    True
    updateInteractionPointsAfter Cmd_goal_type_context{}             = Bool
    False
    updateInteractionPointsAfter Cmd_goal_type_context_infer{}       = Bool
    False
    updateInteractionPointsAfter Cmd_goal_type_context_check{}       = Bool
    False
    updateInteractionPointsAfter Cmd_show_module_contents{}          = Bool
    False
    updateInteractionPointsAfter Cmd_make_case{}                     = Bool
    True
    updateInteractionPointsAfter Cmd_compute{}                       = Bool
    False
    updateInteractionPointsAfter Cmd_why_in_scope{}                  = Bool
    False
    updateInteractionPointsAfter Cmd_why_in_scope_toplevel{}         = Bool
    False
    updateInteractionPointsAfter Cmd_show_version{}                  = Bool
    False
    updateInteractionPointsAfter Cmd_abort{}                         = Bool
    False
    updateInteractionPointsAfter Cmd_exit{}                          = Bool
    False

    -- | Interpret an interaction

    interpret :: Interaction -> CommandM ()

    interpret :: Interaction' Range -> StateT CommandState TCM ()
    interpret (Cmd_load [Char]
    m [[Char]]
    argv) =
      [Char]
    -> [[Char]]
    -> Bool
    -> Mode
    -> (CheckResult -> StateT CommandState TCM ())
    -> StateT CommandState TCM ()
    forall a.
    [Char]
    -> [[Char]]
    -> Bool
    -> Mode
    -> (CheckResult -> CommandM a)
    -> CommandM a
    cmd_load' [Char]
    m [[Char]]
    argv Bool
    True Mode
    mode ((CheckResult -> StateT CommandState TCM ())
     -> StateT CommandState TCM ())
    -> (CheckResult -> StateT CommandState TCM ())
    -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ \CheckResult
    _ -> Interaction' Range -> StateT CommandState TCM ()
    interpret (Interaction' Range -> StateT CommandState TCM ())
    -> Interaction' Range -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Interaction' Range
    forall range. Rewrite -> Interaction' range
    Cmd_metas Rewrite
    AsIs
      where
      mode :: Mode
    mode = Mode
    TypeCheck

    interpret (Cmd_compile CompilerBackend
    backend [Char]
    file [[Char]]
    argv) =
      [Char]
    -> [[Char]]
    -> Bool
    -> Mode
    -> (CheckResult -> StateT CommandState TCM ())
    -> StateT CommandState TCM ()
    forall a.
    [Char]
    -> [[Char]]
    -> Bool
    -> Mode
    -> (CheckResult -> CommandM a)
    -> CommandM a
    cmd_load' [Char]
    file [[Char]]
    argv Bool
    allowUnsolved Mode
    mode ((CheckResult -> StateT CommandState TCM ())
     -> StateT CommandState TCM ())
    -> (CheckResult -> StateT CommandState TCM ())
    -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ CheckResult
    checkResult -> do
        [TCWarning]
    mw <- TCM [TCWarning] -> StateT CommandState TCM [TCWarning]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM [TCWarning] -> StateT CommandState TCM [TCWarning])
    -> TCM [TCWarning] -> StateT CommandState TCM [TCWarning]
    forall a b. (a -> b) -> a -> b
    $ [TCWarning] -> TCM [TCWarning]
    forall (m :: * -> *). HasOptions m => [TCWarning] -> m [TCWarning]
    applyFlagsToTCWarnings ([TCWarning] -> TCM [TCWarning]) -> [TCWarning] -> TCM [TCWarning]
    forall a b. (a -> b) -> a -> b
    $ CheckResult -> [TCWarning]
    crWarnings CheckResult
    checkResult
        case [TCWarning]
    mw of
          [] -> do
            TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ case CompilerBackend
    backend of
              CompilerBackend
    LaTeX                    -> [Char] -> IsMain -> CheckResult -> TCMT IO ()
    callBackend [Char]
    "LaTeX" IsMain
    IsMain CheckResult
    checkResult
              CompilerBackend
    QuickLaTeX               -> [Char] -> IsMain -> CheckResult -> TCMT IO ()
    callBackend [Char]
    "LaTeX" IsMain
    IsMain CheckResult
    checkResult
              OtherBackend [Char]
    "GHCNoMain" -> [Char] -> IsMain -> CheckResult -> TCMT IO ()
    callBackend [Char]
    "GHC" IsMain
    NotMain CheckResult
    checkResult   -- for backwards compatibility
              OtherBackend [Char]
    b           -> [Char] -> IsMain -> CheckResult -> TCMT IO ()
    callBackend [Char]
    b IsMain
    IsMain CheckResult
    checkResult
            DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> (WarningsAndNonFatalErrors -> DisplayInfo)
    -> WarningsAndNonFatalErrors
    -> StateT CommandState TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CompilerBackend -> WarningsAndNonFatalErrors -> DisplayInfo
    Info_CompilationOk CompilerBackend
    backend (WarningsAndNonFatalErrors -> StateT CommandState TCM ())
    -> StateT CommandState TCM WarningsAndNonFatalErrors
    -> StateT CommandState TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO WarningsAndNonFatalErrors
    -> StateT CommandState TCM WarningsAndNonFatalErrors
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCMT IO WarningsAndNonFatalErrors
    B.getWarningsAndNonFatalErrors
          w :: [TCWarning]
    w@(TCWarning
    _:[TCWarning]
    _) -> DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ Info_Error -> DisplayInfo
    Info_Error (Info_Error -> DisplayInfo) -> Info_Error -> DisplayInfo
    forall a b. (a -> b) -> a -> b
    $ [TCWarning] -> Info_Error
    Info_CompilationError [TCWarning]
    w
      where
      allowUnsolved :: Bool
    allowUnsolved = CompilerBackend
    backend CompilerBackend -> [CompilerBackend] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [CompilerBackend
    LaTeX, CompilerBackend
    QuickLaTeX]
      mode :: Mode
    mode | CompilerBackend
    QuickLaTeX <- CompilerBackend
    backend = Mode
    ScopeCheck
           | Bool
    otherwise             = Mode
    TypeCheck

    interpret Interaction' Range
    Cmd_constraints =
        DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> ([OutputForm Expr Expr] -> DisplayInfo)
    -> [OutputForm Expr Expr]
    -> StateT CommandState TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [OutputForm Expr Expr] -> DisplayInfo
    Info_Constraints ([OutputForm Expr Expr] -> StateT CommandState TCM ())
    -> StateT CommandState TCM [OutputForm Expr Expr]
    -> StateT CommandState TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO [OutputForm Expr Expr]
    -> StateT CommandState TCM [OutputForm Expr Expr]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCMT IO [OutputForm Expr Expr]
    B.getConstraints

    interpret (Cmd_metas Rewrite
    norm) = do
      Goals
    ms <- TCMT IO Goals -> StateT CommandState TCM Goals
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Goals -> StateT CommandState TCM Goals)
    -> TCMT IO Goals -> StateT CommandState TCM Goals
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Rewrite -> TCMT IO Goals
    B.getGoals' Rewrite
    norm (Rewrite -> Rewrite -> Rewrite
    forall a. Ord a => a -> a -> a
    max Rewrite
    Simplified Rewrite
    norm)
      DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> (WarningsAndNonFatalErrors -> DisplayInfo)
    -> WarningsAndNonFatalErrors
    -> StateT CommandState TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Goals -> WarningsAndNonFatalErrors -> DisplayInfo
    Info_AllGoalsWarnings Goals
    ms (WarningsAndNonFatalErrors -> StateT CommandState TCM ())
    -> StateT CommandState TCM WarningsAndNonFatalErrors
    -> StateT CommandState TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO WarningsAndNonFatalErrors
    -> StateT CommandState TCM WarningsAndNonFatalErrors
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCMT IO WarningsAndNonFatalErrors
    B.getWarningsAndNonFatalErrors

    interpret (Cmd_show_module_contents_toplevel Rewrite
    norm [Char]
    s) =
      StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a. CommandM a -> CommandM a
    atTopLevel (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Range -> [Char] -> StateT CommandState TCM ()
    showModuleContents Rewrite
    norm Range
    forall a. Range' a
    noRange [Char]
    s

    interpret (Cmd_search_about_toplevel Rewrite
    norm [Char]
    s) =
      StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a. CommandM a -> CommandM a
    atTopLevel (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Range -> [Char] -> StateT CommandState TCM ()
    searchAbout Rewrite
    norm Range
    forall a. Range' a
    noRange [Char]
    s

    interpret (Cmd_solveAll Rewrite
    norm)        = Rewrite -> Maybe InteractionId -> StateT CommandState TCM ()
    solveInstantiatedGoals Rewrite
    norm Maybe InteractionId
    forall a. Maybe a
    Nothing
    interpret (Cmd_solveOne Rewrite
    norm InteractionId
    ii Range
    _ [Char]
    _) = Rewrite -> Maybe InteractionId -> StateT CommandState TCM ()
    solveInstantiatedGoals Rewrite
    norm' (InteractionId -> Maybe InteractionId
    forall a. a -> Maybe a
    Just InteractionId
    ii)
      -- `solveOne` is called via `agda2-maybe-normalised` which does not use
      -- AsIs < Simplified < Normalised but rather Simplified < Instantiated < Normalised
      -- So we remap the Rewrite modifiers to match solveAll's behaviour.
      -- NB: instantiate is called in getSolvedInteractionPoints no matter what.
      where norm' :: Rewrite
    norm' = case Rewrite
    norm of
                      Rewrite
    Simplified   -> Rewrite
    AsIs
                      Rewrite
    Instantiated -> Rewrite
    Simplified
                      Rewrite
    _            -> Rewrite
    norm

    interpret (Cmd_infer_toplevel Rewrite
    norm [Char]
    s) = do
      (Maybe CPUTime
    time, Expr
    expr) <- (Expr -> TCM Expr) -> [Char] -> CommandM (Maybe CPUTime, Expr)
    forall a. (Expr -> TCM a) -> [Char] -> CommandM (Maybe CPUTime, a)
    parseAndDoAtToplevel (Rewrite -> Expr -> TCM Expr
    B.typeInCurrent Rewrite
    norm) [Char]
    s
      CommandState
    state <- StateT CommandState TCM CommandState
    forall s (m :: * -> *). MonadState s m => m s
    get
      DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ CommandState -> Maybe CPUTime -> Expr -> DisplayInfo
    Info_InferredType CommandState
    state Maybe CPUTime
    time Expr
    expr

    interpret (Cmd_compute_toplevel ComputeMode
    cmode [Char]
    s) = do
      (Maybe CPUTime
    time, Expr
    expr) <- (Expr -> TCM Expr) -> [Char] -> CommandM (Maybe CPUTime, Expr)
    forall a. (Expr -> TCM a) -> [Char] -> CommandM (Maybe CPUTime, a)
    parseAndDoAtToplevel Expr -> TCM Expr
    action (ComputeMode -> [Char] -> [Char]
    B.computeWrapInput ComputeMode
    cmode [Char]
    s)
      CommandState
    state <- StateT CommandState TCM CommandState
    forall s (m :: * -> *). MonadState s m => m s
    get
      DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ CommandState -> ComputeMode -> Maybe CPUTime -> Expr -> DisplayInfo
    Info_NormalForm CommandState
    state ComputeMode
    cmode Maybe CPUTime
    time Expr
    expr
        where
        action :: Expr -> TCM Expr
    action = TCM Expr -> TCM Expr
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    allowNonTerminatingReductions
               (TCM Expr -> TCM Expr) -> (Expr -> TCM Expr) -> Expr -> TCM Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (if ComputeMode -> Bool
    B.computeIgnoreAbstract ComputeMode
    cmode then TCM Expr -> TCM Expr
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode else TCM Expr -> TCM Expr
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode)
               (TCM Expr -> TCM Expr) -> (Expr -> TCM Expr) -> Expr -> TCM Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ComputeMode -> Expr -> TCM Expr
    B.evalInCurrent ComputeMode
    cmode
    -- interpret (Cmd_compute_toplevel cmode s) =
    --   parseAndDoAtToplevel action Info_NormalForm $ computeWrapInput cmode s
    --   where
    --   action = allowNonTerminatingReductions
    --          . (if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode)
    --          . (B.showComputed cmode <=< B.evalInCurrent)

    interpret (ShowImplicitArgs Bool
    showImpl) = do
      CommandLineOptions
    opts <- TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      CommandLineOptions -> StateT CommandState TCM ()
    setCommandLineOpts (CommandLineOptions -> StateT CommandState TCM ())
    -> CommandLineOptions -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $
        CommandLineOptions
    opts { optPragmaOptions :: PragmaOptions
    optPragmaOptions =
                 (CommandLineOptions -> PragmaOptions
    optPragmaOptions CommandLineOptions
    opts) { optShowImplicit :: Bool
    optShowImplicit = Bool
    showImpl } }

    interpret Interaction' Range
    ToggleImplicitArgs = do
      CommandLineOptions
    opts <- TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      let ps :: PragmaOptions
    ps = CommandLineOptions -> PragmaOptions
    optPragmaOptions CommandLineOptions
    opts
      CommandLineOptions -> StateT CommandState TCM ()
    setCommandLineOpts (CommandLineOptions -> StateT CommandState TCM ())
    -> CommandLineOptions -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $
        CommandLineOptions
    opts { optPragmaOptions :: PragmaOptions
    optPragmaOptions =
                 PragmaOptions
    ps { optShowImplicit :: Bool
    optShowImplicit = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> Bool
    optShowImplicit PragmaOptions
    ps } }

    interpret (ShowIrrelevantArgs Bool
    showIrr) = do
      CommandLineOptions
    opts <- TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      CommandLineOptions -> StateT CommandState TCM ()
    setCommandLineOpts (CommandLineOptions -> StateT CommandState TCM ())
    -> CommandLineOptions -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $
        CommandLineOptions
    opts { optPragmaOptions :: PragmaOptions
    optPragmaOptions =
                 (CommandLineOptions -> PragmaOptions
    optPragmaOptions CommandLineOptions
    opts) { optShowIrrelevant :: Bool
    optShowIrrelevant = Bool
    showIrr } }

    interpret Interaction' Range
    ToggleIrrelevantArgs = do
      CommandLineOptions
    opts <- TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      let ps :: PragmaOptions
    ps = CommandLineOptions -> PragmaOptions
    optPragmaOptions CommandLineOptions
    opts
      CommandLineOptions -> StateT CommandState TCM ()
    setCommandLineOpts (CommandLineOptions -> StateT CommandState TCM ())
    -> CommandLineOptions -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $
        CommandLineOptions
    opts { optPragmaOptions :: PragmaOptions
    optPragmaOptions =
                 PragmaOptions
    ps { optShowIrrelevant :: Bool
    optShowIrrelevant = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> Bool
    optShowIrrelevant PragmaOptions
    ps } }

    interpret (Cmd_load_highlighting_info [Char]
    source) = do
      HighlightingLevel
    l <- (TCEnv -> HighlightingLevel)
    -> StateT CommandState TCM HighlightingLevel
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> HighlightingLevel
    envHighlightingLevel
      Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (HighlightingLevel
    l HighlightingLevel -> HighlightingLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    /= HighlightingLevel
    None) (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        -- Make sure that the include directories have
        -- been set.
        CommandLineOptions -> StateT CommandState TCM ()
    setCommandLineOpts (CommandLineOptions -> StateT CommandState TCM ())
    -> StateT CommandState TCM CommandLineOptions
    -> StateT CommandState TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
        [Response]
    resp <- TCMT IO [Response] -> StateT CommandState TCM [Response]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [Response] -> StateT CommandState TCM [Response])
    -> TCMT IO [Response] -> StateT CommandState TCM [Response]
    forall a b. (a -> b) -> a -> b
    $ IO [Response] -> TCMT IO [Response]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [Response] -> TCMT IO [Response])
    -> (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
        -> IO [Response])
    -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> TCMT IO [Response]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> IO [Response]
    tellToUpdateHighlighting (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
     -> TCMT IO [Response])
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    -> TCMT IO [Response]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
          Bool
    ex        <- IO Bool -> TCMT IO Bool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> TCMT IO Bool) -> IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO Bool
    doesFileExist [Char]
    source
          SourceFile
    absSource <- IO SourceFile -> TCMT IO SourceFile
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SourceFile -> TCMT IO SourceFile)
    -> IO SourceFile -> TCMT IO SourceFile
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> SourceFile
    SourceFile (AbsolutePath -> SourceFile) -> IO AbsolutePath -> IO SourceFile
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> IO AbsolutePath
    absolute [Char]
    source
          if Bool
    ex
            then
               do
                  Source
    src <- SourceFile -> TCM Source
    Imp.parseSource SourceFile
    absSource
                  let m :: TopLevelModuleName
    m = Source -> TopLevelModuleName
    Imp.srcModuleName Source
    src
                  TopLevelModuleName
    -> SourceFile -> Maybe TopLevelModuleName -> TCMT IO ()
    checkModuleName TopLevelModuleName
    m SourceFile
    absSource Maybe TopLevelModuleName
    forall a. Maybe a
    Nothing
                  Maybe ModuleInfo
    mmi <- TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
    forall (m :: * -> *).
    ReadTCState m =>
    TopLevelModuleName -> m (Maybe ModuleInfo)
    getVisitedModule TopLevelModuleName
    m
                  case Maybe ModuleInfo
    mmi of
                    Maybe ModuleInfo
    Nothing -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    forall a. Maybe a
    Nothing
                    Just ModuleInfo
    mi ->
                      if Text -> Hash
    hashText (Source -> Text
    Imp.srcText Source
    src) Hash -> Hash -> Bool
    forall a. Eq a => a -> a -> Bool
    == Interface -> Hash
    iSourceHash (ModuleInfo -> Interface
    miInterface ModuleInfo
    mi)
                        then do
                          ModuleToSource
    modFile <- Lens' ModuleToSource TCState -> TCMT IO ModuleToSource
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' ModuleToSource TCState
    stModuleToSource
                          HighlightingMethod
    method  <- Lens' HighlightingMethod TCEnv -> TCMT IO HighlightingMethod
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' HighlightingMethod TCEnv
    eHighlightingMethod
                          Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
     -> TCMT
          IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)))
    -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    forall a b. (a -> b) -> a -> b
    $ (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    forall a. a -> Maybe a
    Just (Interface -> HighlightingInfo
    iHighlighting (Interface -> HighlightingInfo) -> Interface -> HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    mi, HighlightingMethod
    method, ModuleToSource
    modFile)
                        else
                          Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    forall a. Maybe a
    Nothing
                TCMT
      IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    -> (TCErr
        -> TCMT
             IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)))
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    _ -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    forall a. Maybe a
    Nothing
            else
              Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    forall a. Maybe a
    Nothing
        (Response -> StateT CommandState TCM ())
    -> [Response] -> StateT CommandState TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Response -> StateT CommandState TCM ()
    putResponse [Response]
    resp

    interpret (Cmd_tokenHighlighting [Char]
    source Remove
    remove) = do
      Maybe HighlightingInfo
    info <- do HighlightingLevel
    l <- (TCEnv -> HighlightingLevel)
    -> StateT CommandState TCM HighlightingLevel
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> HighlightingLevel
    envHighlightingLevel
                 if HighlightingLevel
    l HighlightingLevel -> HighlightingLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    == HighlightingLevel
    None
                   then Maybe HighlightingInfo
    -> StateT CommandState TCM (Maybe HighlightingInfo)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe HighlightingInfo
    forall a. Maybe a
    Nothing
                   else do
                     AbsolutePath
    source' <- IO AbsolutePath -> StateT CommandState TCM AbsolutePath
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ([Char] -> IO AbsolutePath
    absolute [Char]
    source)
                     TCMT IO (Maybe HighlightingInfo)
    -> StateT CommandState TCM (Maybe HighlightingInfo)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO (Maybe HighlightingInfo)
     -> StateT CommandState TCM (Maybe HighlightingInfo))
    -> TCMT IO (Maybe HighlightingInfo)
    -> StateT CommandState TCM (Maybe HighlightingInfo)
    forall a b. (a -> b) -> a -> b
    $ (HighlightingInfo -> Maybe HighlightingInfo
    forall a. a -> Maybe a
    Just (HighlightingInfo -> Maybe HighlightingInfo)
    -> TCMT IO HighlightingInfo -> TCMT IO (Maybe HighlightingInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> AbsolutePath -> TCMT IO HighlightingInfo
    generateTokenInfo AbsolutePath
    source')
                               TCMT IO (Maybe HighlightingInfo)
    -> (TCErr -> TCMT IO (Maybe HighlightingInfo))
    -> TCMT IO (Maybe HighlightingInfo)
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    _ ->
                            Maybe HighlightingInfo -> TCMT IO (Maybe HighlightingInfo)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe HighlightingInfo
    forall a. Maybe a
    Nothing
          StateT CommandState TCM (Maybe HighlightingInfo)
    -> StateT CommandState TCM ()
    -> StateT CommandState TCM (Maybe HighlightingInfo)
    forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
    `finally`
        case Remove
    remove of
          Remove
    Remove -> IO () -> StateT CommandState TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> StateT CommandState TCM ())
    -> IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO ()
    removeFile [Char]
    source
          Remove
    Keep   -> () -> StateT CommandState TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      case Maybe HighlightingInfo
    info of
        Just HighlightingInfo
    info' -> TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ RemoveTokenBasedHighlighting -> HighlightingInfo -> TCMT IO ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    RemoveHighlighting HighlightingInfo
    info'
        Maybe HighlightingInfo
    Nothing    -> () -> StateT CommandState TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    interpret (Cmd_highlight InteractionId
    ii Range
    rng [Char]
    s) = do
      HighlightingLevel
    l <- (TCEnv -> HighlightingLevel)
    -> StateT CommandState TCM HighlightingLevel
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> HighlightingLevel
    envHighlightingLevel
      Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (HighlightingLevel
    l HighlightingLevel -> HighlightingLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    /= HighlightingLevel
    None) (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        ScopeInfo
    scope <- InteractionId -> CommandM ScopeInfo
    getOldInteractionScope InteractionId
    ii
        InteractionId -> StateT CommandState TCM ()
    removeOldInteractionScope InteractionId
    ii
        ExceptT Info_Error TCM () -> StateT CommandState TCM ()
    handle (ExceptT Info_Error TCM () -> StateT CommandState TCM ())
    -> ExceptT Info_Error TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          Expr
    parsed <- Info_Error -> TCM Expr -> ExceptT Info_Error TCM Expr
    forall a. Info_Error -> TCM a -> ExceptT Info_Error TCM a
    try (InteractionId -> Info_Error
    Info_HighlightingParseError InteractionId
    ii) (TCM Expr -> ExceptT Info_Error TCM Expr)
    -> TCM Expr -> ExceptT Info_Error TCM Expr
    forall a b. (a -> b) -> a -> b
    $
                 Range -> [Char] -> TCM Expr
    B.parseExpr Range
    rng [Char]
    s
          Expr
    expr <- Info_Error -> TCM Expr -> ExceptT Info_Error TCM Expr
    forall a. Info_Error -> TCM a -> ExceptT Info_Error TCM a
    try (InteractionId -> Info_Error
    Info_HighlightingScopeCheckError InteractionId
    ii) (TCM Expr -> ExceptT Info_Error TCM Expr)
    -> TCM Expr -> ExceptT Info_Error TCM Expr
    forall a b. (a -> b) -> a -> b
    $
                 ScopeInfo -> Expr -> ScopeM (AbsOfCon Expr)
    forall c. ToAbstract c => ScopeInfo -> c -> ScopeM (AbsOfCon c)
    concreteToAbstract ScopeInfo
    scope Expr
    parsed
          TCMT IO () -> ExceptT Info_Error TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> ExceptT Info_Error TCM ())
    -> TCMT IO () -> ExceptT Info_Error TCM ()
    forall a b. (a -> b) -> a -> b
    $ RemoveTokenBasedHighlighting -> HighlightingInfo -> TCMT IO ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting (HighlightingInfo -> TCMT IO ())
    -> TCMT IO HighlightingInfo -> TCMT IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                   Range -> [Char] -> TCMT IO HighlightingInfo
    generateTokenInfoFromString Range
    rng [Char]
    s
          TCMT IO () -> ExceptT Info_Error TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> ExceptT Info_Error TCM ())
    -> TCMT IO () -> ExceptT Info_Error TCM ()
    forall a b. (a -> b) -> a -> b
    $ Expr -> TCMT IO ()
    highlightExpr Expr
    expr
      where
        handle :: ExceptT Info_Error TCM () -> CommandM ()
        handle :: ExceptT Info_Error TCM () -> StateT CommandState TCM ()
    handle ExceptT Info_Error TCM ()
    m = do
          Either Info_Error ()
    res <- TCM (Either Info_Error ())
    -> StateT CommandState TCM (Either Info_Error ())
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM (Either Info_Error ())
     -> StateT CommandState TCM (Either Info_Error ()))
    -> TCM (Either Info_Error ())
    -> StateT CommandState TCM (Either Info_Error ())
    forall a b. (a -> b) -> a -> b
    $ ExceptT Info_Error TCM () -> TCM (Either Info_Error ())
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT ExceptT Info_Error TCM ()
    m
          case Either Info_Error ()
    res of
            Left Info_Error
    err -> DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ Info_Error -> DisplayInfo
    Info_Error Info_Error
    err
            Right ()
    _ -> () -> StateT CommandState TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        try :: Info_Error -> TCM a -> ExceptT Info_Error TCM a
        try :: forall a. Info_Error -> TCM a -> ExceptT Info_Error TCM a
    try Info_Error
    err TCM a
    m = TCMT IO (Either Info_Error a) -> ExceptT Info_Error TCM a
    forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
    ExceptT (TCMT IO (Either Info_Error a) -> ExceptT Info_Error TCM a)
    -> TCMT IO (Either Info_Error a) -> ExceptT Info_Error TCM a
    forall a b. (a -> b) -> a -> b
    $ do
          ((TCErr -> Info_Error) -> Either TCErr a -> Either Info_Error a
    forall a c b. (a -> c) -> Either a b -> Either c b
    mapLeft (Info_Error -> TCErr -> Info_Error
    forall a b. a -> b -> a
    const Info_Error
    err) (Either TCErr a -> Either Info_Error a)
    -> TCMT IO (Either TCErr a) -> TCMT IO (Either Info_Error a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM a -> TCMT IO (Either TCErr a)
    forall a. TCM a -> TCM (Either TCErr a)
    freshTCM TCM a
    m) TCMT IO (Either Info_Error a)
    -> (TCErr -> TCMT IO (Either Info_Error a))
    -> TCMT IO (Either Info_Error a)
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    _ -> Either Info_Error a -> TCMT IO (Either Info_Error a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Info_Error -> Either Info_Error a
    forall a b. a -> Either a b
    Left Info_Error
    err)
          -- freshTCM to avoid scope checking creating new interaction points

    interpret (Cmd_give   UseForce
    force InteractionId
    ii Range
    rng [Char]
    s) = UseForce
    -> InteractionId
    -> Range
    -> [Char]
    -> GiveRefine
    -> StateT CommandState TCM ()
    give_gen UseForce
    force InteractionId
    ii Range
    rng [Char]
    s GiveRefine
    Give
    interpret (Cmd_refine InteractionId
    ii Range
    rng [Char]
    s) = UseForce
    -> InteractionId
    -> Range
    -> [Char]
    -> GiveRefine
    -> StateT CommandState TCM ()
    give_gen UseForce
    WithoutForce InteractionId
    ii Range
    rng [Char]
    s GiveRefine
    Refine

    interpret (Cmd_intro Bool
    pmLambda InteractionId
    ii Range
    rng [Char]
    _) = do
      [[Char]]
    ss <- TCMT IO [[Char]] -> StateT CommandState TCM [[Char]]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [[Char]] -> StateT CommandState TCM [[Char]])
    -> TCMT IO [[Char]] -> StateT CommandState TCM [[Char]]
    forall a b. (a -> b) -> a -> b
    $ Bool -> InteractionId -> TCMT IO [[Char]]
    B.introTactic Bool
    pmLambda InteractionId
    ii
      (forall a. TCM a -> TCM a)
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    liftCommandMT (InteractionId -> TCMT IO x -> TCMT IO x
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii) (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ case [[Char]]
    ss of
        []    -> do
          DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ DisplayInfo
    Info_Intro_NotFound
        [[Char]
    s]   -> UseForce
    -> InteractionId
    -> Range
    -> [Char]
    -> GiveRefine
    -> StateT CommandState TCM ()
    give_gen UseForce
    WithoutForce InteractionId
    ii Range
    rng [Char]
    s GiveRefine
    Intro
        [Char]
    _:[Char]
    _:[[Char]]
    _ -> do
          DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> DisplayInfo
    Info_Intro_ConstructorUnknown [[Char]]
    ss

    interpret (Cmd_refine_or_intro Bool
    pmLambda InteractionId
    ii Range
    r [Char]
    s) = Interaction' Range -> StateT CommandState TCM ()
    interpret (Interaction' Range -> StateT CommandState TCM ())
    -> Interaction' Range -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $
      let s' :: [Char]
    s' = [Char] -> [Char]
    trim [Char]
    s
      in (if [Char] -> Bool
    forall a. Null a => a -> Bool
    null [Char]
    s' then Bool -> InteractionId -> Range -> [Char] -> Interaction' Range
    forall range.
    Bool -> InteractionId -> range -> [Char] -> Interaction' range
    Cmd_intro Bool
    pmLambda else InteractionId -> Range -> [Char] -> Interaction' Range
    forall range.
    InteractionId -> range -> [Char] -> Interaction' range
    Cmd_refine) InteractionId
    ii Range
    r [Char]
    s'

    interpret (Cmd_autoOne InteractionId
    ii Range
    rng [Char]
    hint) = do
      -- Andreas, 2014-07-05 Issue 1226:
      -- Save the state to have access to even those interaction ids
      -- that Auto solves (since Auto gives the solution right away).
      TCState
    st <- StateT CommandState TCM TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
      (Maybe CPUTime
    time , AutoResult
    res) <- CommandM AutoResult -> CommandM (Maybe CPUTime, AutoResult)
    forall a. CommandM a -> CommandM (Maybe CPUTime, a)
    maybeTimed (CommandM AutoResult -> CommandM (Maybe CPUTime, AutoResult))
    -> CommandM AutoResult -> CommandM (Maybe CPUTime, AutoResult)
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> Range -> [Char] -> CommandM AutoResult
    forall (tcm :: * -> *).
    MonadTCM tcm =>
    InteractionId -> Range -> [Char] -> tcm AutoResult
    Auto.auto InteractionId
    ii Range
    rng [Char]
    hint
      case AutoResult -> AutoProgress
    autoProgress AutoResult
    res of
       Solutions [(InteractionId, [Char])]
    sols -> do
        TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "auto" Int
    10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Auto produced the following solutions " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [(InteractionId, [Char])] -> [Char]
    forall a. Show a => a -> [Char]
    show [(InteractionId, [Char])]
    sols
        [(InteractionId, [Char])]
    -> ((InteractionId, [Char]) -> StateT CommandState TCM ())
    -> StateT CommandState TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(InteractionId, [Char])]
    sols (((InteractionId, [Char]) -> StateT CommandState TCM ())
     -> StateT CommandState TCM ())
    -> ((InteractionId, [Char]) -> StateT CommandState TCM ())
    -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ \(InteractionId
    ii', [Char]
    sol) -> do
          -- Andreas, 2014-07-05 Issue 1226:
          -- For highlighting, Resp_GiveAction needs to access
          -- the @oldInteractionScope@s of the interaction points solved by Auto.
          -- We dig them out from the state before Auto was invoked.
          InteractionId -> ScopeInfo -> StateT CommandState TCM ()
    insertOldInteractionScope InteractionId
    ii' (ScopeInfo -> StateT CommandState TCM ())
    -> CommandM ScopeInfo -> StateT CommandState TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM ScopeInfo -> CommandM ScopeInfo
    forall a. TCM a -> CommandM a
    liftLocalState (TCState -> TCMT IO ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    st TCMT IO () -> TCM ScopeInfo -> TCM ScopeInfo
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> InteractionId -> TCM ScopeInfo
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m ScopeInfo
    getInteractionScope InteractionId
    ii')
          -- Andreas, 2014-07-07: NOT TRUE:
          -- -- Andreas, 2014-07-05: The following should be obsolete,
          -- -- as Auto has removed the interaction points already:
          -- modifyTheInteractionPoints $ filter (/= ii)
          Response -> StateT CommandState TCM ()
    putResponse (Response -> StateT CommandState TCM ())
    -> Response -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> GiveResult -> Response
    Resp_GiveAction InteractionId
    ii' (GiveResult -> Response) -> GiveResult -> Response
    forall a b. (a -> b) -> a -> b
    $ [Char] -> GiveResult
    Give_String [Char]
    sol
        -- Andreas, 2014-07-07: Remove the interaction points in one go.
        ([InteractionId] -> [InteractionId]) -> StateT CommandState TCM ()
    modifyTheInteractionPoints ([InteractionId] -> [InteractionId] -> [InteractionId]
    forall a. Eq a => [a] -> [a] -> [a]
    List.\\ (((InteractionId, [Char]) -> InteractionId)
    -> [(InteractionId, [Char])] -> [InteractionId]
    forall a b. (a -> b) -> [a] -> [b]
    map (InteractionId, [Char]) -> InteractionId
    forall a b. (a, b) -> a
    fst [(InteractionId, [Char])]
    sols))
        case AutoResult -> Maybe [Char]
    autoMessage AutoResult
    res of
         Maybe [Char]
    Nothing  -> Interaction' Range -> StateT CommandState TCM ()
    interpret (Interaction' Range -> StateT CommandState TCM ())
    -> Interaction' Range -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Interaction' Range
    forall range. Rewrite -> Interaction' range
    Cmd_metas Rewrite
    AsIs
         Just [Char]
    msg -> DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> DisplayInfo
    Info_Auto [Char]
    msg
       FunClauses [[Char]]
    cs -> do
        case AutoResult -> Maybe [Char]
    autoMessage AutoResult
    res of
         Maybe [Char]
    Nothing  -> () -> StateT CommandState TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
         Just [Char]
    msg -> DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> DisplayInfo
    Info_Auto [Char]
    msg
        Response -> StateT CommandState TCM ()
    putResponse (Response -> StateT CommandState TCM ())
    -> Response -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> MakeCaseVariant -> [[Char]] -> Response
    Resp_MakeCase InteractionId
    ii MakeCaseVariant
    R.Function [[Char]]
    cs
       Refinement [Char]
    s -> UseForce
    -> InteractionId
    -> Range
    -> [Char]
    -> GiveRefine
    -> StateT CommandState TCM ()
    give_gen UseForce
    WithoutForce InteractionId
    ii Range
    rng [Char]
    s GiveRefine
    Refine
      StateT CommandState TCM ()
    -> (CPUTime -> StateT CommandState TCM ())
    -> Maybe CPUTime
    -> StateT CommandState TCM ()
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (() -> StateT CommandState TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) (DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> (CPUTime -> DisplayInfo)
    -> CPUTime
    -> StateT CommandState TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CPUTime -> DisplayInfo
    Info_Time) Maybe CPUTime
    time

    interpret Interaction' Range
    Cmd_autoAll = do
      [InteractionId]
    iis <- StateT CommandState TCM [InteractionId]
    forall (m :: * -> *). ReadTCState m => m [InteractionId]
    getInteractionPoints
      Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([InteractionId] -> Bool
    forall a. Null a => a -> Bool
    null [InteractionId]
    iis) (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        let time :: Int
    time = Int
    1000 Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `div` [InteractionId] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [InteractionId]
    iis
        TCState
    st <- StateT CommandState TCM TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
        [[InteractionId]]
    solved <- [InteractionId]
    -> (InteractionId -> StateT CommandState TCM [InteractionId])
    -> StateT CommandState TCM [[InteractionId]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [InteractionId]
    iis ((InteractionId -> StateT CommandState TCM [InteractionId])
     -> StateT CommandState TCM [[InteractionId]])
    -> (InteractionId -> StateT CommandState TCM [InteractionId])
    -> StateT CommandState TCM [[InteractionId]]
    forall a b. (a -> b) -> a -> b
    $ \ InteractionId
    ii -> do
          Range
    rng <- InteractionId -> StateT CommandState TCM Range
    forall (m :: * -> *).
    (MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
    InteractionId -> m Range
    getInteractionRange InteractionId
    ii
          AutoResult
    res <- InteractionId -> Range -> [Char] -> CommandM AutoResult
    forall (tcm :: * -> *).
    MonadTCM tcm =>
    InteractionId -> Range -> [Char] -> tcm AutoResult
    Auto.auto InteractionId
    ii Range
    rng ([Char]
    "-t " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    time [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "ms")
          case AutoResult -> AutoProgress
    autoProgress AutoResult
    res of
            Solutions [(InteractionId, [Char])]
    sols -> [(InteractionId, [Char])]
    -> ((InteractionId, [Char])
        -> StateT CommandState TCM InteractionId)
    -> StateT CommandState TCM [InteractionId]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(InteractionId, [Char])]
    sols (((InteractionId, [Char]) -> StateT CommandState TCM InteractionId)
     -> StateT CommandState TCM [InteractionId])
    -> ((InteractionId, [Char])
        -> StateT CommandState TCM InteractionId)
    -> StateT CommandState TCM [InteractionId]
    forall a b. (a -> b) -> a -> b
    $ \ (InteractionId
    jj, [Char]
    s) -> do
                ScopeInfo
    oldInteractionScope <- TCM ScopeInfo -> CommandM ScopeInfo
    forall a. TCM a -> CommandM a
    liftLocalState (TCState -> TCMT IO ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    st TCMT IO () -> TCM ScopeInfo -> TCM ScopeInfo
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> InteractionId -> TCM ScopeInfo
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m ScopeInfo
    getInteractionScope InteractionId
    jj)
                InteractionId -> ScopeInfo -> StateT CommandState TCM ()
    insertOldInteractionScope InteractionId
    jj ScopeInfo
    oldInteractionScope
                Response -> StateT CommandState TCM ()
    putResponse (Response -> StateT CommandState TCM ())
    -> Response -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> GiveResult -> Response
    Resp_GiveAction InteractionId
    ii (GiveResult -> Response) -> GiveResult -> Response
    forall a b. (a -> b) -> a -> b
    $ [Char] -> GiveResult
    Give_String [Char]
    s
                InteractionId -> StateT CommandState TCM InteractionId
    forall (m :: * -> *) a. Monad m => a -> m a
    return InteractionId
    jj
            AutoProgress
    _ -> [InteractionId] -> StateT CommandState TCM [InteractionId]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        ([InteractionId] -> [InteractionId]) -> StateT CommandState TCM ()
    modifyTheInteractionPoints ([InteractionId] -> [InteractionId] -> [InteractionId]
    forall a. Eq a => [a] -> [a] -> [a]
    List.\\ [[InteractionId]] -> [InteractionId]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[InteractionId]]
    solved)

    interpret (Cmd_context Rewrite
    norm InteractionId
    ii Range
    _ [Char]
    _) =
      DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> ([ResponseContextEntry] -> DisplayInfo)
    -> [ResponseContextEntry]
    -> StateT CommandState TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InteractionId -> [ResponseContextEntry] -> DisplayInfo
    Info_Context InteractionId
    ii ([ResponseContextEntry] -> StateT CommandState TCM ())
    -> StateT CommandState TCM [ResponseContextEntry]
    -> StateT CommandState TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM [ResponseContextEntry]
    -> StateT CommandState TCM [ResponseContextEntry]
    forall a. TCM a -> CommandM a
    liftLocalState (Rewrite -> InteractionId -> TCM [ResponseContextEntry]
    B.getResponseContext Rewrite
    norm InteractionId
    ii)

    interpret (Cmd_helper_function Rewrite
    norm InteractionId
    ii Range
    rng [Char]
    s) = do
      -- Create type of application of new helper function that would solve the goal.
      OutputConstraint' Expr Expr
    helperType <- TCM (OutputConstraint' Expr Expr)
    -> CommandM (OutputConstraint' Expr Expr)
    forall a. TCM a -> CommandM a
    liftLocalState (TCM (OutputConstraint' Expr Expr)
     -> CommandM (OutputConstraint' Expr Expr))
    -> TCM (OutputConstraint' Expr Expr)
    -> CommandM (OutputConstraint' Expr Expr)
    forall a b. (a -> b) -> a -> b
    $ InteractionId
    -> TCM (OutputConstraint' Expr Expr)
    -> TCM (OutputConstraint' Expr Expr)
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM (OutputConstraint' Expr Expr)
     -> TCM (OutputConstraint' Expr Expr))
    -> TCM (OutputConstraint' Expr Expr)
    -> TCM (OutputConstraint' Expr Expr)
    forall a b. (a -> b) -> a -> b
    $ TCM (OutputConstraint' Expr Expr)
    -> TCM (OutputConstraint' Expr Expr)
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM (OutputConstraint' Expr Expr)
     -> TCM (OutputConstraint' Expr Expr))
    -> TCM (OutputConstraint' Expr Expr)
    -> TCM (OutputConstraint' Expr Expr)
    forall a b. (a -> b) -> a -> b
    $ Rewrite
    -> InteractionId
    -> Range
    -> [Char]
    -> TCM (OutputConstraint' Expr Expr)
    B.metaHelperType Rewrite
    norm InteractionId
    ii Range
    rng [Char]
    s
      DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> GoalDisplayInfo -> DisplayInfo
    Info_GoalSpecific InteractionId
    ii (OutputConstraint' Expr Expr -> GoalDisplayInfo
    Goal_HelperFunction OutputConstraint' Expr Expr
    helperType)

    interpret (Cmd_infer Rewrite
    norm InteractionId
    ii Range
    rng [Char]
    s) = do
      Expr
    expr <- TCM Expr -> CommandM Expr
    forall a. TCM a -> CommandM a
    liftLocalState (TCM Expr -> CommandM Expr) -> TCM Expr -> CommandM Expr
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> TCM Expr -> TCM Expr
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> Rewrite -> Expr -> TCM Expr
    B.typeInMeta InteractionId
    ii Rewrite
    norm (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< InteractionId -> Range -> [Char] -> TCM Expr
    B.parseExprIn InteractionId
    ii Range
    rng [Char]
    s
      DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> GoalDisplayInfo -> DisplayInfo
    Info_GoalSpecific InteractionId
    ii (Expr -> GoalDisplayInfo
    Goal_InferredType Expr
    expr)

    interpret (Cmd_goal_type Rewrite
    norm InteractionId
    ii Range
    _ [Char]
    _) =
      DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> GoalDisplayInfo -> DisplayInfo
    Info_GoalSpecific InteractionId
    ii (Rewrite -> GoalDisplayInfo
    Goal_CurrentGoal Rewrite
    norm)

    interpret (Cmd_elaborate_give Rewrite
    norm InteractionId
    ii Range
    rng [Char]
    s) =
      UseForce
    -> InteractionId
    -> Range
    -> [Char]
    -> GiveRefine
    -> StateT CommandState TCM ()
    give_gen UseForce
    WithoutForce InteractionId
    ii Range
    rng [Char]
    s (GiveRefine -> StateT CommandState TCM ())
    -> GiveRefine -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> GiveRefine
    ElaborateGive Rewrite
    norm

    interpret (Cmd_goal_type_context Rewrite
    norm InteractionId
    ii Range
    rng [Char]
    s) =
      GoalTypeAux
    -> Rewrite
    -> InteractionId
    -> Range
    -> [Char]
    -> StateT CommandState TCM ()
    cmd_goal_type_context_and GoalTypeAux
    GoalOnly Rewrite
    norm InteractionId
    ii Range
    rng [Char]
    s

    interpret (Cmd_goal_type_context_infer Rewrite
    norm InteractionId
    ii Range
    rng [Char]
    s) = do
      -- In case of the empty expression to type, don't fail with
      -- a stupid parse error, but just fall back to
      -- Cmd_goal_type_context.
      GoalTypeAux
    aux <- if (Char -> Bool) -> [Char] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    Char.isSpace [Char]
    s
                then GoalTypeAux -> StateT CommandState TCM GoalTypeAux
    forall (m :: * -> *) a. Monad m => a -> m a
    return GoalTypeAux
    GoalOnly
                else do
                  Expr
    typ <- TCM Expr -> CommandM Expr
    forall a. TCM a -> CommandM a
    liftLocalState
                        (TCM Expr -> CommandM Expr) -> TCM Expr -> CommandM Expr
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> TCM Expr -> TCM Expr
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii
                        (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> Rewrite -> Expr -> TCM Expr
    B.typeInMeta InteractionId
    ii Rewrite
    norm (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< InteractionId -> Range -> [Char] -> TCM Expr
    B.parseExprIn InteractionId
    ii Range
    rng [Char]
    s
                  GoalTypeAux -> StateT CommandState TCM GoalTypeAux
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> GoalTypeAux
    GoalAndHave Expr
    typ)
      GoalTypeAux
    -> Rewrite
    -> InteractionId
    -> Range
    -> [Char]
    -> StateT CommandState TCM ()
    cmd_goal_type_context_and GoalTypeAux
    aux Rewrite
    norm InteractionId
    ii Range
    rng [Char]
    s

    interpret (Cmd_goal_type_context_check Rewrite
    norm InteractionId
    ii Range
    rng [Char]
    s) = do
      Term
    term <- TCM Term -> CommandM Term
    forall a. TCM a -> CommandM a
    liftLocalState (TCM Term -> CommandM Term) -> TCM Term -> CommandM Term
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> TCM Term -> TCM Term
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM Term -> TCM Term) -> TCM Term -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ do
        Expr
    expr <- InteractionId -> Range -> [Char] -> TCM Expr
    B.parseExprIn InteractionId
    ii Range
    rng [Char]
    s
        OutputConstraint Expr InteractionId
    goal <- Rewrite
    -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
    B.typeOfMeta Rewrite
    AsIs InteractionId
    ii
        Term
    term <- case OutputConstraint Expr InteractionId
    goal of
          OfType InteractionId
    _ Expr
    ty -> Expr -> Type -> TCM Term
    checkExpr Expr
    expr (Type -> TCM Term) -> TCMT IO Type -> TCM Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr -> TCMT IO Type
    isType_ Expr
    ty
          OutputConstraint Expr InteractionId
    _           -> TCM Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Rewrite -> Term -> TCM Term
    forall t.
    (Reduce t, Simplify t, Instantiate t, Normalise t) =>
    Rewrite -> t -> TCM t
    B.normalForm Rewrite
    norm Term
    term
      GoalTypeAux
    -> Rewrite
    -> InteractionId
    -> Range
    -> [Char]
    -> StateT CommandState TCM ()
    cmd_goal_type_context_and (Term -> GoalTypeAux
    GoalAndElaboration Term
    term) Rewrite
    norm InteractionId
    ii Range
    rng [Char]
    s

    interpret (Cmd_show_module_contents Rewrite
    norm InteractionId
    ii Range
    rng [Char]
    s) =
      (forall a. TCM a -> TCM a)
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    liftCommandMT (InteractionId -> TCMT IO x -> TCMT IO x
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii) (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Range -> [Char] -> StateT CommandState TCM ()
    showModuleContents Rewrite
    norm Range
    rng [Char]
    s

    interpret (Cmd_why_in_scope_toplevel [Char]
    s) =
      StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a. CommandM a -> CommandM a
    atTopLevel (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> StateT CommandState TCM ()
    whyInScope [Char]
    s

    interpret (Cmd_why_in_scope InteractionId
    ii Range
    _range [Char]
    s) =
      (forall a. TCM a -> TCM a)
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    liftCommandMT (InteractionId -> TCMT IO x -> TCMT IO x
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii) (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> StateT CommandState TCM ()
    whyInScope [Char]
    s

    interpret (Cmd_make_case InteractionId
    ii Range
    rng [Char]
    s) = do
      (QName
    f, CaseContext
    casectxt, [Clause]
    cs) <- TCMT IO (QName, CaseContext, [Clause])
    -> StateT CommandState TCM (QName, CaseContext, [Clause])
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO (QName, CaseContext, [Clause])
     -> StateT CommandState TCM (QName, CaseContext, [Clause]))
    -> TCMT IO (QName, CaseContext, [Clause])
    -> StateT CommandState TCM (QName, CaseContext, [Clause])
    forall a b. (a -> b) -> a -> b
    $ InteractionId
    -> Range -> [Char] -> TCMT IO (QName, CaseContext, [Clause])
    makeCase InteractionId
    ii Range
    rng [Char]
    s
      (forall a. TCM a -> TCM a)
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    liftCommandMT (InteractionId -> TCMT IO x -> TCMT IO x
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii) (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        Telescope
    tel <- TCM Telescope -> StateT CommandState TCM Telescope
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Telescope -> StateT CommandState TCM Telescope)
    -> TCM Telescope -> StateT CommandState TCM Telescope
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> TCM Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection (QName -> ModuleName
    qnameModule QName
    f) -- don't shadow the names in this telescope
        UnicodeOrAscii
    unicode <- (TCState -> UnicodeOrAscii)
    -> StateT CommandState TCM UnicodeOrAscii
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC ((TCState -> UnicodeOrAscii)
     -> StateT CommandState TCM UnicodeOrAscii)
    -> (TCState -> UnicodeOrAscii)
    -> StateT CommandState TCM UnicodeOrAscii
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> UnicodeOrAscii
    optUseUnicode (PragmaOptions -> UnicodeOrAscii)
    -> (TCState -> PragmaOptions) -> TCState -> UnicodeOrAscii
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> PragmaOptions
    forall a. LensPragmaOptions a => a -> PragmaOptions
    getPragmaOptions
        [Doc]
    pcs      :: [Doc]      <- TCM [Doc] -> StateT CommandState TCM [Doc]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM [Doc] -> StateT CommandState TCM [Doc])
    -> TCM [Doc] -> StateT CommandState TCM [Doc]
    forall a b. (a -> b) -> a -> b
    $ TCM [Doc] -> TCM [Doc]
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM [Doc] -> TCM [Doc]) -> TCM [Doc] -> TCM [Doc]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCM [Doc] -> TCM [Doc]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (TCM [Doc] -> TCM [Doc]) -> TCM [Doc] -> TCM [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Clause -> TCMT IO Doc) -> [Clause] -> TCM [Doc]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Clause -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [Clause]
    cs
        let [[Char]]
    pcs' :: [String]    = (Doc -> [Char]) -> [Doc] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    List.map (UnicodeOrAscii -> CaseContext -> [Char] -> [Char]
    extlam_dropName UnicodeOrAscii
    unicode CaseContext
    casectxt ([Char] -> [Char]) -> (Doc -> [Char]) -> Doc -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> [Char]
    decorate) [Doc]
    pcs
        TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "interaction.case" Int
    60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat
          [ TCMT IO Doc
    "InteractionTop.Cmd_make_case"
          , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    TCP.nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat
            [ TCMT IO Doc
    "cs   = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat ((Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [Clause]
    cs)
            , TCMT IO Doc
    "pcs  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat ((Doc -> TCMT IO Doc) -> [Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Doc]
    pcs)
            , TCMT IO Doc
    "pcs' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat (([Char] -> TCMT IO Doc) -> [[Char]] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    TCP.text [[Char]]
    pcs')
            ]
          ]
        TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "interaction.case" Int
    90 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat
          [ TCMT IO Doc
    "InteractionTop.Cmd_make_case"
          , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    TCP.nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat
            [ TCMT IO Doc
    "cs   = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    TCP.text ([Clause] -> [Char]
    forall a. Show a => a -> [Char]
    show [Clause]
    cs)
            ]
          ]
        Response -> StateT CommandState TCM ()
    putResponse (Response -> StateT CommandState TCM ())
    -> Response -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> MakeCaseVariant -> [[Char]] -> Response
    Resp_MakeCase InteractionId
    ii (CaseContext -> MakeCaseVariant
    makeCaseVariant CaseContext
    casectxt) [[Char]]
    pcs'
      where
        decorate :: Doc -> [Char]
    decorate = Style -> Doc -> [Char]
    renderStyle (Style
    style { mode :: Mode
    mode = Mode
    OneLineMode })

        makeCaseVariant :: CaseContext -> MakeCaseVariant
        makeCaseVariant :: CaseContext -> MakeCaseVariant
    makeCaseVariant CaseContext
    Nothing = MakeCaseVariant
    R.Function
        makeCaseVariant Just{}  = MakeCaseVariant
    R.ExtendedLambda

        -- very dirty hack, string manipulation by dropping the function name
        -- and replacing the last " = " with " -> ". It's important not to replace
        -- the equal sign in named implicit with an arrow!
        extlam_dropName :: UnicodeOrAscii -> CaseContext -> String -> String
        extlam_dropName :: UnicodeOrAscii -> CaseContext -> [Char] -> [Char]
    extlam_dropName UnicodeOrAscii
    _ CaseContext
    Nothing [Char]
    x = [Char]
    x
        extlam_dropName UnicodeOrAscii
    glyphMode Just{}  [Char]
    x
            = [[Char]] -> [Char]
    unwords ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [[Char]]
    forall a. [a] -> [a]
    reverse ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [[Char]]
    replEquals ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [[Char]]
    forall a. [a] -> [a]
    reverse ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ Int -> [[Char]] -> [[Char]]
    forall a. Int -> [a] -> [a]
    drop Int
    1 ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [[Char]]
    words [Char]
    x
          where
            arrow :: [Char]
    arrow = Doc -> [Char]
    render (Doc -> [Char]) -> Doc -> [Char]
    forall a b. (a -> b) -> a -> b
    $ SpecialCharacters -> Doc
    _arrow (SpecialCharacters -> Doc) -> SpecialCharacters -> Doc
    forall a b. (a -> b) -> a -> b
    $ UnicodeOrAscii -> SpecialCharacters
    specialCharactersForGlyphs UnicodeOrAscii
    glyphMode
            replEquals :: [[Char]] -> [[Char]]
    replEquals ([Char]
    "=" : [[Char]]
    ws) = [Char]
    arrow [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : [[Char]]
    ws
            replEquals ([Char]
    w   : [[Char]]
    ws) = [Char]
    w [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : [[Char]] -> [[Char]]
    replEquals [[Char]]
    ws
            replEquals []         = []

    interpret (Cmd_compute ComputeMode
    cmode InteractionId
    ii Range
    rng [Char]
    s) = do
      Expr
    expr <- TCM Expr -> CommandM Expr
    forall a. TCM a -> CommandM a
    liftLocalState (TCM Expr -> CommandM Expr) -> TCM Expr -> CommandM Expr
    forall a b. (a -> b) -> a -> b
    $ do
        Expr
    e <- InteractionId -> Range -> [Char] -> TCM Expr
    B.parseExprIn InteractionId
    ii Range
    rng ([Char] -> TCM Expr) -> [Char] -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ ComputeMode -> [Char] -> [Char]
    B.computeWrapInput ComputeMode
    cmode [Char]
    s
        InteractionId -> TCM Expr -> TCM Expr
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ Bool -> (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall a. Bool -> (a -> a) -> a -> a
    applyWhen (ComputeMode -> Bool
    B.computeIgnoreAbstract ComputeMode
    cmode) TCM Expr -> TCM Expr
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ ComputeMode -> Expr -> TCM Expr
    B.evalInCurrent ComputeMode
    cmode Expr
    e
      DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> GoalDisplayInfo -> DisplayInfo
    Info_GoalSpecific InteractionId
    ii (ComputeMode -> Expr -> GoalDisplayInfo
    Goal_NormalForm ComputeMode
    cmode Expr
    expr)

    interpret Interaction' Range
    Cmd_show_version = DisplayInfo -> StateT CommandState TCM ()
    display_info DisplayInfo
    Info_Version

    interpret Interaction' Range
    Cmd_abort = () -> StateT CommandState TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    interpret Interaction' Range
    Cmd_exit  = () -> StateT CommandState TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | Solved goals already instantiated internally
    -- The second argument potentially limits it to one specific goal.
    solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
    solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> StateT CommandState TCM ()
    solveInstantiatedGoals Rewrite
    norm Maybe InteractionId
    mii = do
      -- Andreas, 2016-10-23 issue #2280: throw away meta elims.
      [(InteractionId, Expr)]
    out <- TCMT IO [(InteractionId, Expr)]
    -> StateT CommandState TCM [(InteractionId, Expr)]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [(InteractionId, Expr)]
     -> StateT CommandState TCM [(InteractionId, Expr)])
    -> TCMT IO [(InteractionId, Expr)]
    -> StateT CommandState TCM [(InteractionId, Expr)]
    forall a b. (a -> b) -> a -> b
    $ (TCEnv -> TCEnv)
    -> TCMT IO [(InteractionId, Expr)]
    -> TCMT IO [(InteractionId, Expr)]
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e { envPrintMetasBare :: Bool
    envPrintMetasBare = Bool
    True }) (TCMT IO [(InteractionId, Expr)]
     -> TCMT IO [(InteractionId, Expr)])
    -> TCMT IO [(InteractionId, Expr)]
    -> TCMT IO [(InteractionId, Expr)]
    forall a b. (a -> b) -> a -> b
    $ do
        [(InteractionId, MetaId, Expr)]
    sip <- Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
    B.getSolvedInteractionPoints Bool
    False Rewrite
    norm
               -- only solve metas which have a proper instantiation, i.e., not another meta
        let sip' :: [(InteractionId, MetaId, Expr)]
    sip' = ([(InteractionId, MetaId, Expr)]
     -> [(InteractionId, MetaId, Expr)])
    -> (InteractionId
        -> [(InteractionId, MetaId, Expr)]
        -> [(InteractionId, MetaId, Expr)])
    -> Maybe InteractionId
    -> [(InteractionId, MetaId, Expr)]
    -> [(InteractionId, MetaId, Expr)]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [(InteractionId, MetaId, Expr)] -> [(InteractionId, MetaId, Expr)]
    forall a. a -> a
    id (\ InteractionId
    ii -> ((InteractionId, MetaId, Expr) -> Bool)
    -> [(InteractionId, MetaId, Expr)]
    -> [(InteractionId, MetaId, Expr)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((InteractionId
    ii InteractionId -> InteractionId -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (InteractionId -> Bool)
    -> ((InteractionId, MetaId, Expr) -> InteractionId)
    -> (InteractionId, MetaId, Expr)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (InteractionId, MetaId, Expr) -> InteractionId
    forall a b c. (a, b, c) -> a
    fst3)) Maybe InteractionId
    mii [(InteractionId, MetaId, Expr)]
    sip
        ((InteractionId, MetaId, Expr) -> TCMT IO (InteractionId, Expr))
    -> [(InteractionId, MetaId, Expr)]
    -> TCMT IO [(InteractionId, Expr)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (InteractionId, MetaId, Expr) -> TCMT IO (InteractionId, Expr)
    forall {m :: * -> *} {a} {a}.
    (MonadTrace m, ToConcrete a, MonadStConcreteNames m, HasOptions m,
     HasBuiltins m, MonadDebug m) =>
    (a, MetaId, a) -> m (a, ConOfAbs a)
    prt [(InteractionId, MetaId, Expr)]
    sip'
      Response -> StateT CommandState TCM ()
    putResponse (Response -> StateT CommandState TCM ())
    -> Response -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [(InteractionId, Expr)] -> Response
    Resp_SolveAll [(InteractionId, Expr)]
    out
      where
          prt :: (a, MetaId, a) -> m (a, ConOfAbs a)
    prt (a
    i, MetaId
    m, a
    e) = do
            Closure Range
    mi <- MetaVariable -> Closure Range
    getMetaInfo (MetaVariable -> Closure Range)
    -> m MetaVariable -> m (Closure Range)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
            ConOfAbs a
    e' <- Closure Range -> m (ConOfAbs a) -> m (ConOfAbs a)
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m, MonadTrace m) =>
    Closure Range -> m a -> m a
    withMetaInfo Closure Range
    mi (m (ConOfAbs a) -> m (ConOfAbs a))
    -> m (ConOfAbs a) -> m (ConOfAbs a)
    forall a b. (a -> b) -> a -> b
    $ Precedence -> a -> m (ConOfAbs a)
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    Precedence -> a -> m (ConOfAbs a)
    abstractToConcreteCtx Precedence
    TopCtx a
    e
            (a, ConOfAbs a) -> m (a, ConOfAbs a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    i, ConOfAbs a
    e')

    -- | @cmd_load' file argv unsolvedOk cmd@
    --   loads the module in file @file@,
    --   using @argv@ as the command-line options.
    --
    -- If type checking completes without any exceptions having been
    -- encountered then the command @cmd r@ is executed, where @r@ is the
    -- result of 'Imp.typeCheckMain'.

    cmd_load'
      :: FilePath  -- ^ File to load into interaction.
      -> [String]  -- ^ Arguments to Agda for loading this file
      -> Bool      -- ^ Allow unsolved meta-variables?
      -> Mode      -- ^ Full type-checking, or only scope-checking?
      -> (CheckResult -> CommandM a)
                   -- ^ Continuation after successful loading.
      -> CommandM a
    cmd_load' :: forall a.
    [Char]
    -> [[Char]]
    -> Bool
    -> Mode
    -> (CheckResult -> CommandM a)
    -> CommandM a
    cmd_load' [Char]
    file [[Char]]
    argv Bool
    unsolvedOK Mode
    mode CheckResult -> CommandM a
    cmd = do
        AbsolutePath
    fp <- IO AbsolutePath -> StateT CommandState TCM AbsolutePath
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO AbsolutePath -> StateT CommandState TCM AbsolutePath)
    -> IO AbsolutePath -> StateT CommandState TCM AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO AbsolutePath
    absolute [Char]
    file
        Bool
    ex <- IO Bool -> StateT CommandState TCM Bool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> StateT CommandState TCM Bool)
    -> IO Bool -> StateT CommandState TCM Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO Bool
    doesFileExist ([Char] -> IO Bool) -> [Char] -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> [Char]
    filePath AbsolutePath
    fp
        Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    ex (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> StateT CommandState TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> StateT CommandState TCM ())
    -> TypeError -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "The file " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    file [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " was not found."

        -- Forget the previous "current file" and interaction points.
        (CommandState -> CommandState) -> StateT CommandState TCM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
    -> (CommandState -> CommandState) -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ CommandState
    st -> CommandState
    st { theInteractionPoints :: [InteractionId]
    theInteractionPoints = []
                            , theCurrentFile :: Maybe CurrentFile
    theCurrentFile       = Maybe CurrentFile
    forall a. Maybe a
    Nothing
                            }

        ClockTime
    t <- IO ClockTime -> StateT CommandState TCM ClockTime
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO ClockTime -> StateT CommandState TCM ClockTime)
    -> IO ClockTime -> StateT CommandState TCM ClockTime
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO ClockTime
    getModificationTime [Char]
    file

        -- Update the status. Because the "current file" is not set the
        -- status is not "Checked".
        StateT CommandState TCM ()
    displayStatus

        -- Reset the state, preserving options and decoded modules. Note
        -- that if the include directories have changed, then the decoded
        -- modules are reset by TCM.setCommandLineOptions' below.
        TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCMT IO ()
    resetState

        -- Clear the info buffer to make room for information about which
        -- module is currently being type-checked.
        Response -> StateT CommandState TCM ()
    putResponse Response
    Resp_ClearRunningInfo

        -- Remove any prior syntax highlighting.
        Response -> StateT CommandState TCM ()
    putResponse (TokenBased -> Response
    Resp_ClearHighlighting TokenBased
    NotOnlyTokenBased)

        -- Parse the file.
        --
        -- Note that options are set below.
        Source
    src <- TCM Source -> StateT CommandState TCM Source
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Source -> StateT CommandState TCM Source)
    -> TCM Source -> StateT CommandState TCM Source
    forall a b. (a -> b) -> a -> b
    $ SourceFile -> TCM Source
    Imp.parseSource (AbsolutePath -> SourceFile
    SourceFile AbsolutePath
    fp)

        -- Store the warnings.
        [TCWarning]
    warnings <- Lens' [TCWarning] TCState -> StateT CommandState TCM [TCWarning]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [TCWarning] TCState
    stTCWarnings

        -- All options are reset when a file is reloaded, including the
        -- choice of whether or not to display implicit arguments.
        CommandLineOptions
    opts0 <- (CommandState -> CommandLineOptions)
    -> StateT CommandState TCM CommandLineOptions
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets CommandState -> CommandLineOptions
    optionsOnReload
        [Backend]
    backends <- Lens' [Backend] TCState -> StateT CommandState TCM [Backend]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [Backend] TCState
    stBackends
        Either [Char] ([Backend], CommandLineOptions)
    z <- OptM ([Backend], CommandLineOptions)
    -> StateT
         CommandState TCM (Either [Char] ([Backend], CommandLineOptions))
    forall (m :: * -> *) opts.
    Monad m =>
    OptM opts -> m (Either [Char] opts)
    runOptM (OptM ([Backend], CommandLineOptions)
     -> StateT
          CommandState TCM (Either [Char] ([Backend], CommandLineOptions)))
    -> OptM ([Backend], CommandLineOptions)
    -> StateT
         CommandState TCM (Either [Char] ([Backend], CommandLineOptions))
    forall a b. (a -> b) -> a -> b
    $ [Backend]
    -> [[Char]]
    -> CommandLineOptions
    -> OptM ([Backend], CommandLineOptions)
    parseBackendOptions [Backend]
    backends [[Char]]
    argv CommandLineOptions
    opts0
        case Either [Char] ([Backend], CommandLineOptions)
    z of
          Left [Char]
    err   -> TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    GenericError [Char]
    err
          Right ([Backend]
    _, CommandLineOptions
    opts) -> do
            CommandLineOptions
    opts <- TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM CommandLineOptions
     -> StateT CommandState TCM CommandLineOptions)
    -> TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions -> TCM CommandLineOptions
    addTrustedExecutables CommandLineOptions
    opts
            let update :: PragmaOptions -> PragmaOptions
    update PragmaOptions
    o = PragmaOptions
    o { optAllowUnsolved :: Bool
    optAllowUnsolved = Bool
    unsolvedOK Bool -> Bool -> Bool
    && PragmaOptions -> Bool
    optAllowUnsolved PragmaOptions
    o}
                root :: AbsolutePath
    root     = AbsolutePath -> TopLevelModuleName -> AbsolutePath
    projectRoot AbsolutePath
    fp (TopLevelModuleName -> AbsolutePath)
    -> TopLevelModuleName -> AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ Source -> TopLevelModuleName
    Imp.srcModuleName Source
    src
            TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> CommandLineOptions -> TCMT IO ()
    TCM.setCommandLineOptions' AbsolutePath
    root (CommandLineOptions -> TCMT IO ())
    -> CommandLineOptions -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (PragmaOptions -> PragmaOptions)
    -> CommandLineOptions -> CommandLineOptions
    forall a.
    LensPragmaOptions a =>
    (PragmaOptions -> PragmaOptions) -> a -> a
    mapPragmaOptions PragmaOptions -> PragmaOptions
    update CommandLineOptions
    opts

        -- Restore the warnings that were saved above.
        Lens' [TCWarning] TCState
    -> ([TCWarning] -> [TCWarning]) -> StateT CommandState TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens Lens' [TCWarning] TCState
    stTCWarnings ([TCWarning] -> [TCWarning] -> [TCWarning]
    forall a. [a] -> [a] -> [a]
    ++ [TCWarning]
    warnings)

        CheckResult
    ok <- TCMT IO CheckResult -> StateT CommandState TCM CheckResult
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO CheckResult -> StateT CommandState TCM CheckResult)
    -> TCMT IO CheckResult -> StateT CommandState TCM CheckResult
    forall a b. (a -> b) -> a -> b
    $ Mode -> Source -> TCMT IO CheckResult
    Imp.typeCheckMain Mode
    mode Source
    src

        -- The module type checked. If the file was not changed while the
        -- type checker was running then the interaction points and the
        -- "current file" are stored.
        ClockTime
    t' <- IO ClockTime -> StateT CommandState TCM ClockTime
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO ClockTime -> StateT CommandState TCM ClockTime)
    -> IO ClockTime -> StateT CommandState TCM ClockTime
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO ClockTime
    getModificationTime [Char]
    file
        Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (ClockTime
    t ClockTime -> ClockTime -> Bool
    forall a. Eq a => a -> a -> Bool
    == ClockTime
    t') (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          [InteractionId]
    is <- TCM [InteractionId] -> StateT CommandState TCM [InteractionId]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM [InteractionId] -> StateT CommandState TCM [InteractionId])
    -> TCM [InteractionId] -> StateT CommandState TCM [InteractionId]
    forall a b. (a -> b) -> a -> b
    $ [InteractionId] -> TCM [InteractionId]
    forall (m :: * -> *).
    (MonadInteractionPoints m, MonadError TCErr m, MonadFail m) =>
    [InteractionId] -> m [InteractionId]
    sortInteractionPoints ([InteractionId] -> TCM [InteractionId])
    -> TCM [InteractionId] -> TCM [InteractionId]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM [InteractionId]
    forall (m :: * -> *). ReadTCState m => m [InteractionId]
    getInteractionPoints
          (CommandState -> CommandState) -> StateT CommandState TCM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
    -> (CommandState -> CommandState) -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ \CommandState
    st -> CommandState
    st { theInteractionPoints :: [InteractionId]
    theInteractionPoints = [InteractionId]
    is
                             , theCurrentFile :: Maybe CurrentFile
    theCurrentFile       = CurrentFile -> Maybe CurrentFile
    forall a. a -> Maybe a
    Just (CurrentFile -> Maybe CurrentFile)
    -> CurrentFile -> Maybe CurrentFile
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> [[Char]] -> ClockTime -> CurrentFile
    CurrentFile AbsolutePath
    fp [[Char]]
    argv ClockTime
    t
                             }

        CheckResult -> CommandM a
    cmd CheckResult
    ok

    -- | Set 'envCurrentPath' to 'theCurrentFile', if any.
    withCurrentFile :: CommandM a -> CommandM a
    withCurrentFile :: forall a. CommandM a -> CommandM a
    withCurrentFile CommandM a
    m = do
      Maybe AbsolutePath
    mfile <- (CommandState -> Maybe AbsolutePath)
    -> StateT CommandState TCM (Maybe AbsolutePath)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ((CommandState -> Maybe AbsolutePath)
     -> StateT CommandState TCM (Maybe AbsolutePath))
    -> (CommandState -> Maybe AbsolutePath)
    -> StateT CommandState TCM (Maybe AbsolutePath)
    forall a b. (a -> b) -> a -> b
    $ (CurrentFile -> AbsolutePath)
    -> Maybe CurrentFile -> Maybe AbsolutePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap CurrentFile -> AbsolutePath
    currentFilePath (Maybe CurrentFile -> Maybe AbsolutePath)
    -> (CommandState -> Maybe CurrentFile)
    -> CommandState
    -> Maybe AbsolutePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CommandState -> Maybe CurrentFile
    theCurrentFile
      (TCEnv -> TCEnv) -> CommandM a -> CommandM a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e { envCurrentPath :: Maybe AbsolutePath
    envCurrentPath = Maybe AbsolutePath
    mfile }) CommandM a
    m

    atTopLevel :: CommandM a -> CommandM a
    atTopLevel :: forall a. CommandM a -> CommandM a
    atTopLevel CommandM a
    cmd = (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
    liftCommandMT forall a. TCM a -> TCM a
    B.atTopLevel CommandM a
    cmd

    ---------------------------------------------------------------------------
    -- Giving, refining.

    data GiveRefine = Give | Refine | Intro | ElaborateGive Rewrite
      deriving (GiveRefine -> GiveRefine -> Bool
    (GiveRefine -> GiveRefine -> Bool)
    -> (GiveRefine -> GiveRefine -> Bool) -> Eq GiveRefine
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: GiveRefine -> GiveRefine -> Bool
    $c/= :: GiveRefine -> GiveRefine -> Bool
    == :: GiveRefine -> GiveRefine -> Bool
    $c== :: GiveRefine -> GiveRefine -> Bool
    Eq, Int -> GiveRefine -> [Char] -> [Char]
    [GiveRefine] -> [Char] -> [Char]
    GiveRefine -> [Char]
    (Int -> GiveRefine -> [Char] -> [Char])
    -> (GiveRefine -> [Char])
    -> ([GiveRefine] -> [Char] -> [Char])
    -> Show GiveRefine
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    showList :: [GiveRefine] -> [Char] -> [Char]
    $cshowList :: [GiveRefine] -> [Char] -> [Char]
    show :: GiveRefine -> [Char]
    $cshow :: GiveRefine -> [Char]
    showsPrec :: Int -> GiveRefine -> [Char] -> [Char]
    $cshowsPrec :: Int -> GiveRefine -> [Char] -> [Char]
    Show)

    -- | A "give"-like action (give, refine, etc).
    --
    --   @give_gen force ii rng s give_ref mk_newtxt@
    --   acts on interaction point @ii@
    --   occupying range @rng@,
    --   placing the new content given by string @s@,
    --   and replacing @ii@ by the newly created interaction points
    --   in the state if safety checks pass (unless @force@ is applied).
    give_gen
      :: UseForce       -- ^ Should safety checks be skipped?
      -> InteractionId
      -> Range
      -> String
      -> GiveRefine
      -> CommandM ()
    give_gen :: UseForce
    -> InteractionId
    -> Range
    -> [Char]
    -> GiveRefine
    -> StateT CommandState TCM ()
    give_gen UseForce
    force InteractionId
    ii Range
    rng [Char]
    s0 GiveRefine
    giveRefine = do
      let s :: [Char]
    s = [Char] -> [Char]
    trim [Char]
    s0
      [Char] -> Int -> [Char] -> StateT CommandState TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "interaction.give" Int
    20 ([Char] -> StateT CommandState TCM ())
    -> [Char] -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "give_gen  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s
      -- Andreas, 2015-02-26 if string is empty do nothing rather
      -- than giving a parse error.
      Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Char] -> Bool
    forall a. Null a => a -> Bool
    null [Char]
    s) (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        let give_ref :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    give_ref =
              case GiveRefine
    giveRefine of
                GiveRefine
    Give               -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    B.give
                GiveRefine
    Refine             -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    B.refine
                GiveRefine
    Intro              -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    B.refine
                ElaborateGive Rewrite
    norm -> Rewrite
    -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    B.elaborate_give Rewrite
    norm
        -- save scope of the interaction point (for printing the given expr. later)
        ScopeInfo
    scope     <- InteractionId -> CommandM ScopeInfo
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m ScopeInfo
    getInteractionScope InteractionId
    ii
        -- parse string and "give", obtaining an abstract expression
        -- and newly created interaction points
        (Maybe CPUTime
    time, (Expr
    ae, Expr
    ae0, [InteractionId]
    iis)) <- CommandM (Expr, Expr, [InteractionId])
    -> CommandM (Maybe CPUTime, (Expr, Expr, [InteractionId]))
    forall a. CommandM a -> CommandM (Maybe CPUTime, a)
    maybeTimed (CommandM (Expr, Expr, [InteractionId])
     -> CommandM (Maybe CPUTime, (Expr, Expr, [InteractionId])))
    -> CommandM (Expr, Expr, [InteractionId])
    -> CommandM (Maybe CPUTime, (Expr, Expr, [InteractionId]))
    forall a b. (a -> b) -> a -> b
    $ do
            -- Issue 3000: mark the current hole as solved before giving, to avoid confusing it with potential
            -- new interaction points introduced by the give.
            InteractionId -> StateT CommandState TCM ()
    forall (m :: * -> *).
    MonadInteractionPoints m =>
    InteractionId -> m ()
    removeInteractionPoint InteractionId
    ii
            [InteractionId]
    mis  <- StateT CommandState TCM [InteractionId]
    forall (m :: * -> *). ReadTCState m => m [InteractionId]
    getInteractionPoints
            [Char] -> Int -> [Char] -> StateT CommandState TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "interaction.give" Int
    30 ([Char] -> StateT CommandState TCM ())
    -> [Char] -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "interaction points before = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [InteractionId] -> [Char]
    forall a. Show a => a -> [Char]
    show [InteractionId]
    mis
            Expr
    given <- TCM Expr -> CommandM Expr
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Expr -> CommandM Expr) -> TCM Expr -> CommandM Expr
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> Range -> [Char] -> TCM Expr
    B.parseExprIn InteractionId
    ii Range
    rng [Char]
    s
            Expr
    ae    <- TCM Expr -> CommandM Expr
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Expr -> CommandM Expr) -> TCM Expr -> CommandM Expr
    forall a b. (a -> b) -> a -> b
    $ UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    give_ref UseForce
    force InteractionId
    ii Maybe Range
    forall a. Maybe a
    Nothing Expr
    given
            [InteractionId]
    mis' <- StateT CommandState TCM [InteractionId]
    forall (m :: * -> *). ReadTCState m => m [InteractionId]
    getInteractionPoints
            [Char] -> Int -> [Char] -> StateT CommandState TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "interaction.give" Int
    30 ([Char] -> StateT CommandState TCM ())
    -> [Char] -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "interaction points after = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [InteractionId] -> [Char]
    forall a. Show a => a -> [Char]
    show [InteractionId]
    mis'
            (Expr, Expr, [InteractionId])
    -> CommandM (Expr, Expr, [InteractionId])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr
    ae, Expr
    given, [InteractionId]
    mis' [InteractionId] -> [InteractionId] -> [InteractionId]
    forall a. Eq a => [a] -> [a] -> [a]
    List.\\ [InteractionId]
    mis)
        -- favonia: backup the old scope for highlighting
        InteractionId -> ScopeInfo -> StateT CommandState TCM ()
    insertOldInteractionScope InteractionId
    ii ScopeInfo
    scope
        -- sort the new interaction points and put them into the state
        -- in replacement of the old interaction point
        [InteractionId]
    iis' <- [InteractionId] -> StateT CommandState TCM [InteractionId]
    forall (m :: * -> *).
    (MonadInteractionPoints m, MonadError TCErr m, MonadFail m) =>
    [InteractionId] -> m [InteractionId]
    sortInteractionPoints [InteractionId]
    iis
        ([InteractionId] -> [InteractionId]) -> StateT CommandState TCM ()
    modifyTheInteractionPoints (([InteractionId] -> [InteractionId])
     -> StateT CommandState TCM ())
    -> ([InteractionId] -> [InteractionId])
    -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId
    -> [InteractionId] -> [InteractionId] -> [InteractionId]
    forall {t :: * -> *} {b}.
    (Foldable t, Eq b) =>
    b -> [b] -> t b -> [b]
    replace InteractionId
    ii [InteractionId]
    iis'
        -- print abstract expr
        Expr
    ce        <- ScopeInfo -> Expr -> StateT CommandState TCM (ConOfAbs Expr)
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    ScopeInfo -> a -> m (ConOfAbs a)
    abstractToConcreteScope ScopeInfo
    scope Expr
    ae
        [Char] -> Int -> [[Char]] -> StateT CommandState TCM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Int -> a -> m ()
    reportS [Char]
    "interaction.give" Int
    30
          [ [Char]
    "ce = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Expr -> [Char]
    forall a. Show a => a -> [Char]
    show Expr
    ce
          , [Char]
    "scopePrecedence = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ PrecedenceStack -> [Char]
    forall a. Show a => a -> [Char]
    show (ScopeInfo
    scope ScopeInfo -> Lens' PrecedenceStack ScopeInfo -> PrecedenceStack
    forall o i. o -> Lens' i o -> i
    ^. Lens' PrecedenceStack ScopeInfo
    scopePrecedence)
          ]
        -- if the command was @Give@, use the literal user input;
        -- Andreas, 2014-01-15, see issue 1020:
        -- Refine could solve a goal by introducing the sole constructor
        -- without arguments.  Then there are no interaction metas, but
        -- we still cannot just `give' the user string (which may be empty).
        -- WRONG: also, if no interaction metas were created by @Refine@
        -- WRONG: let literally = (giveRefine == Give || null iis) && rng /= noRange
        -- Ulf, 2015-03-30, if we're doing intro we can't do literal give since
        -- there is nothing in the hole (issue 1892).
        let literally :: Bool
    literally = (GiveRefine
    giveRefine GiveRefine -> GiveRefine -> Bool
    forall a. Eq a => a -> a -> Bool
    == GiveRefine
    Give Bool -> Bool -> Bool
    || GiveRefine
    giveRefine GiveRefine -> GiveRefine -> Bool
    forall a. Eq a => a -> a -> Bool
    == GiveRefine
    Refine) Bool -> Bool -> Bool
    && Expr
    ae Expr -> Expr -> Bool
    forall a. Eq a => a -> a -> Bool
    == Expr
    ae0 Bool -> Bool -> Bool
    && Range
    rng Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Range
    forall a. Range' a
    noRange
        -- Ulf, 2014-01-24: This works for give since we're highlighting the string
        -- that's already in the buffer. Doing it before the give action means that
        -- the highlighting is moved together with the text when the hole goes away.
        -- To make it work for refine we'd have to adjust the ranges.
        Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    literally (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          HighlightingLevel
    l <- (TCEnv -> HighlightingLevel)
    -> StateT CommandState TCM HighlightingLevel
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> HighlightingLevel
    envHighlightingLevel
          Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (HighlightingLevel
    l HighlightingLevel -> HighlightingLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    /= HighlightingLevel
    None) (StateT CommandState TCM () -> StateT CommandState TCM ())
    -> StateT CommandState TCM () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            RemoveTokenBasedHighlighting -> HighlightingInfo -> TCMT IO ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting (HighlightingInfo -> TCMT IO ())
    -> TCMT IO HighlightingInfo -> TCMT IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
              Range -> [Char] -> TCMT IO HighlightingInfo
    generateTokenInfoFromString Range
    rng [Char]
    s
            Expr -> TCMT IO ()
    highlightExpr Expr
    ae
        Response -> StateT CommandState TCM ()
    putResponse (Response -> StateT CommandState TCM ())
    -> Response -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> GiveResult -> Response
    Resp_GiveAction InteractionId
    ii (GiveResult -> Response) -> GiveResult -> Response
    forall a b. (a -> b) -> a -> b
    $ Bool -> Expr -> GiveResult
    mkNewTxt Bool
    literally Expr
    ce
        [Char] -> Int -> [Char] -> StateT CommandState TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "interaction.give" Int
    30 ([Char] -> StateT CommandState TCM ())
    -> [Char] -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "putResponse GiveAction passed"
        -- display new goal set (if not measuring time)
        StateT CommandState TCM ()
    -> (CPUTime -> StateT CommandState TCM ())
    -> Maybe CPUTime
    -> StateT CommandState TCM ()
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Interaction' Range -> StateT CommandState TCM ()
    interpret (Interaction' Range -> StateT CommandState TCM ())
    -> Interaction' Range -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Interaction' Range
    forall range. Rewrite -> Interaction' range
    Cmd_metas Rewrite
    AsIs) (DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> (CPUTime -> DisplayInfo)
    -> CPUTime
    -> StateT CommandState TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CPUTime -> DisplayInfo
    Info_Time) Maybe CPUTime
    time
        [Char] -> Int -> [Char] -> StateT CommandState TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "interaction.give" Int
    30 ([Char] -> StateT CommandState TCM ())
    -> [Char] -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "interpret Cmd_metas passed"
      where
        -- Substitutes xs for x in ys.
        replace :: b -> [b] -> t b -> [b]
    replace b
    x [b]
    xs t b
    ys = (b -> [b]) -> t b -> [b]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (\ b
    y -> if b
    y b -> b -> Bool
    forall a. Eq a => a -> a -> Bool
    == b
    x then [b]
    xs else [b
    y]) t b
    ys
        -- For @Give@ we can replace the ii by the user given input.
        mkNewTxt :: Bool -> Expr -> GiveResult
    mkNewTxt Bool
    True  C.Paren{} = GiveResult
    Give_Paren
        mkNewTxt Bool
    True  Expr
    _         = GiveResult
    Give_NoParen
        -- Otherwise, we replace it by the reified value Agda computed.
        mkNewTxt Bool
    False Expr
    ce        = [Char] -> GiveResult
    Give_String ([Char] -> GiveResult) -> [Char] -> GiveResult
    forall a b. (a -> b) -> a -> b
    $ Expr -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Expr
    ce

    highlightExpr :: A.Expr -> TCM ()
    highlightExpr :: Expr -> TCMT IO ()
    highlightExpr Expr
    e =
      (TCEnv -> TCEnv) -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\TCEnv
    st -> TCEnv
    st { envImportPath :: [TopLevelModuleName]
    envImportPath         = []
                         , envHighlightingLevel :: HighlightingLevel
    envHighlightingLevel  = HighlightingLevel
    NonInteractive
                         , envHighlightingMethod :: HighlightingMethod
    envHighlightingMethod = HighlightingMethod
    Direct }) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        Declaration -> Level -> Bool -> TCMT IO ()
    generateAndPrintSyntaxInfo Declaration
    decl Level
    Full Bool
    True
      where
        dummy :: Name
    dummy = NameId -> [Char] -> Name
    forall a. MkName a => NameId -> a -> Name
    mkName_ (Hash -> ModuleNameHash -> NameId
    NameId Hash
    0 ModuleNameHash
    noModuleNameHash) ([Char]
    "dummy" :: String)
        info :: DefInfo' Expr
    info  = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
    forall t.
    Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
    mkDefInfo (Name -> Name
    nameConcrete Name
    dummy) Fixity'
    noFixity' Access
    PublicAccess IsAbstract
    ConcreteDef (Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e)
        decl :: Declaration
    decl  = KindOfName
    -> DefInfo' Expr
    -> ArgInfo
    -> Maybe [Occurrence]
    -> QName
    -> Expr
    -> Declaration
    A.Axiom KindOfName
    OtherDefName DefInfo' Expr
    info ArgInfo
    defaultArgInfo Maybe [Occurrence]
    forall a. Maybe a
    Nothing (List1 Name -> QName
    qnameFromList (List1 Name -> QName) -> List1 Name -> QName
    forall a b. (a -> b) -> a -> b
    $ Name -> List1 Name
    forall el coll. Singleton el coll => el -> coll
    singleton Name
    dummy) Expr
    e

    -- | Sorts interaction points based on their ranges.

    sortInteractionPoints
      :: (MonadInteractionPoints m, MonadError TCErr m, MonadFail m)
      => [InteractionId] -> m [InteractionId]
    sortInteractionPoints :: forall (m :: * -> *).
    (MonadInteractionPoints m, MonadError TCErr m, MonadFail m) =>
    [InteractionId] -> m [InteractionId]
    sortInteractionPoints [InteractionId]
    is =
      ((InteractionId, Range) -> InteractionId)
    -> [(InteractionId, Range)] -> [InteractionId]
    forall a b. (a -> b) -> [a] -> [b]
    map (InteractionId, Range) -> InteractionId
    forall a b. (a, b) -> a
    fst ([(InteractionId, Range)] -> [InteractionId])
    -> ([(InteractionId, Range)] -> [(InteractionId, Range)])
    -> [(InteractionId, Range)]
    -> [InteractionId]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((InteractionId, Range) -> (InteractionId, Range) -> Ordering)
    -> [(InteractionId, Range)] -> [(InteractionId, Range)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (Range -> Range -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Range -> Range -> Ordering)
    -> ((InteractionId, Range) -> Range)
    -> (InteractionId, Range)
    -> (InteractionId, Range)
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (InteractionId, Range) -> Range
    forall a b. (a, b) -> b
    snd) ([(InteractionId, Range)] -> [InteractionId])
    -> m [(InteractionId, Range)] -> m [InteractionId]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        [InteractionId]
    -> (InteractionId -> m (InteractionId, Range))
    -> m [(InteractionId, Range)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [InteractionId]
    is ((InteractionId -> m (InteractionId, Range))
     -> m [(InteractionId, Range)])
    -> (InteractionId -> m (InteractionId, Range))
    -> m [(InteractionId, Range)]
    forall a b. (a -> b) -> a -> b
    $ \ InteractionId
    i -> do
          (InteractionId
    i,) (Range -> (InteractionId, Range))
    -> m Range -> m (InteractionId, Range)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InteractionId -> m Range
    forall (m :: * -> *).
    (MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
    InteractionId -> m Range
    getInteractionRange InteractionId
    i

    -- | Displays the current goal, the given document, and the current
    --   context.
    --
    --   Should not modify the state.

    cmd_goal_type_context_and :: GoalTypeAux -> Rewrite -> InteractionId -> Range ->
                                 String -> CommandM ()
    cmd_goal_type_context_and :: GoalTypeAux
    -> Rewrite
    -> InteractionId
    -> Range
    -> [Char]
    -> StateT CommandState TCM ()
    cmd_goal_type_context_and GoalTypeAux
    aux Rewrite
    norm InteractionId
    ii Range
    _ [Char]
    _ = do
      [ResponseContextEntry]
    ctx <- TCM [ResponseContextEntry]
    -> StateT CommandState TCM [ResponseContextEntry]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM [ResponseContextEntry]
     -> StateT CommandState TCM [ResponseContextEntry])
    -> TCM [ResponseContextEntry]
    -> StateT CommandState TCM [ResponseContextEntry]
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> InteractionId -> TCM [ResponseContextEntry]
    B.getResponseContext Rewrite
    norm InteractionId
    ii
      [OutputForm Expr Expr]
    constr <- TCMT IO [OutputForm Expr Expr]
    -> StateT CommandState TCM [OutputForm Expr Expr]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [OutputForm Expr Expr]
     -> StateT CommandState TCM [OutputForm Expr Expr])
    -> TCMT IO [OutputForm Expr Expr]
    -> StateT CommandState TCM [OutputForm Expr Expr]
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii TCMT IO MetaId
    -> (MetaId -> TCMT IO [OutputForm Expr Expr])
    -> TCMT IO [OutputForm Expr Expr]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Rewrite -> MetaId -> TCMT IO [OutputForm Expr Expr]
    B.getConstraintsMentioning Rewrite
    norm
      [IPBoundary' Expr]
    boundary <- TCMT IO [IPBoundary' Expr]
    -> StateT CommandState TCM [IPBoundary' Expr]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [IPBoundary' Expr]
     -> StateT CommandState TCM [IPBoundary' Expr])
    -> TCMT IO [IPBoundary' Expr]
    -> StateT CommandState TCM [IPBoundary' Expr]
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> InteractionId -> TCMT IO [IPBoundary' Expr]
    B.getIPBoundary Rewrite
    norm InteractionId
    ii
      DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> GoalDisplayInfo -> DisplayInfo
    Info_GoalSpecific InteractionId
    ii (Rewrite
    -> GoalTypeAux
    -> [ResponseContextEntry]
    -> [IPBoundary' Expr]
    -> [OutputForm Expr Expr]
    -> GoalDisplayInfo
    Goal_GoalType Rewrite
    norm GoalTypeAux
    aux [ResponseContextEntry]
    ctx [IPBoundary' Expr]
    boundary [OutputForm Expr Expr]
    constr)

    -- | Shows all the top-level names in the given module, along with
    -- their types.

    showModuleContents :: Rewrite -> Range -> String -> CommandM ()
    showModuleContents :: Rewrite -> Range -> [Char] -> StateT CommandState TCM ()
    showModuleContents Rewrite
    norm Range
    rng [Char]
    s = do
      ([Name]
    modules, Telescope
    tel, [(Name, Type)]
    types) <- TCMT IO ([Name], Telescope, [(Name, Type)])
    -> StateT CommandState TCM ([Name], Telescope, [(Name, Type)])
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO ([Name], Telescope, [(Name, Type)])
     -> StateT CommandState TCM ([Name], Telescope, [(Name, Type)]))
    -> TCMT IO ([Name], Telescope, [(Name, Type)])
    -> StateT CommandState TCM ([Name], Telescope, [(Name, Type)])
    forall a b. (a -> b) -> a -> b
    $ Rewrite
    -> Range -> [Char] -> TCMT IO ([Name], Telescope, [(Name, Type)])
    B.moduleContents Rewrite
    norm Range
    rng [Char]
    s
      DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Name] -> Telescope -> [(Name, Type)] -> DisplayInfo
    Info_ModuleContents [Name]
    modules Telescope
    tel [(Name, Type)]
    types

    -- | Shows all the top-level names in scope which mention all the given
    -- identifiers in their type.

    searchAbout :: Rewrite -> Range -> String -> CommandM ()
    searchAbout :: Rewrite -> Range -> [Char] -> StateT CommandState TCM ()
    searchAbout Rewrite
    norm Range
    rg [Char]
    names = do
      [Char]
    -> ([Char] -> StateT CommandState TCM ())
    -> StateT CommandState TCM ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull ([Char] -> [Char]
    trim [Char]
    names) (([Char] -> StateT CommandState TCM ())
     -> StateT CommandState TCM ())
    -> ([Char] -> StateT CommandState TCM ())
    -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ [Char]
    trimmedNames -> do
        [(Name, Type)]
    hits <- TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)])
    -> TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)]
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Range -> [Char] -> TCMT IO [(Name, Type)]
    findMentions Rewrite
    norm Range
    rg [Char]
    trimmedNames
        DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [(Name, Type)] -> [Char] -> DisplayInfo
    Info_SearchAbout [(Name, Type)]
    hits [Char]
    trimmedNames

    -- | Explain why something is in scope.

    whyInScope :: String -> CommandM ()
    whyInScope :: [Char] -> StateT CommandState TCM ()
    whyInScope [Char]
    s = do
      Just (CurrentFile AbsolutePath
    file [[Char]]
    _ ClockTime
    _) <- (CommandState -> Maybe CurrentFile)
    -> StateT CommandState TCM (Maybe CurrentFile)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets CommandState -> Maybe CurrentFile
    theCurrentFile
      let cwd :: [Char]
    cwd = [Char] -> [Char]
    takeDirectory (AbsolutePath -> [Char]
    filePath AbsolutePath
    file)
      (Maybe LocalVar
    v, [AbstractName]
    xs, [AbstractModule]
    ms) <- TCM (Maybe LocalVar, [AbstractName], [AbstractModule])
    -> CommandM (Maybe LocalVar, [AbstractName], [AbstractModule])
    forall a. TCM a -> CommandM a
    liftLocalState ([Char] -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule])
    B.whyInScope [Char]
    s)
      DisplayInfo -> StateT CommandState TCM ()
    display_info (DisplayInfo -> StateT CommandState TCM ())
    -> DisplayInfo -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    -> [Char]
    -> Maybe LocalVar
    -> [AbstractName]
    -> [AbstractModule]
    -> DisplayInfo
    Info_WhyInScope [Char]
    s [Char]
    cwd Maybe LocalVar
    v [AbstractName]
    xs [AbstractModule]
    ms

    -- | Sets the command line options and updates the status information.

    setCommandLineOpts :: CommandLineOptions -> CommandM ()
    setCommandLineOpts :: CommandLineOptions -> StateT CommandState TCM ()
    setCommandLineOpts CommandLineOptions
    opts = do
        TCMT IO () -> StateT CommandState TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT CommandState TCM ())
    -> TCMT IO () -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions -> TCMT IO ()
    TCM.setCommandLineOptions CommandLineOptions
    opts
        StateT CommandState TCM ()
    displayStatus

    -- | Computes some status information.
    --
    --   Does not change the state.

    status :: CommandM Status
    status :: CommandM Status
    status = do
      Maybe CurrentFile
    cf       <- (CommandState -> Maybe CurrentFile)
    -> StateT CommandState TCM (Maybe CurrentFile)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets CommandState -> Maybe CurrentFile
    theCurrentFile
      Bool
    showImpl <- TCMT IO Bool -> StateT CommandState TCM Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    showImplicitArguments
      Bool
    showIrr  <- TCMT IO Bool -> StateT CommandState TCM Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    showIrrelevantArguments

      -- Check if the file was successfully type checked, and has not
      -- changed since. Note: This code does not check if any dependencies
      -- have changed, and uses a time stamp to check for changes.
      Bool
    checked  <- TCMT IO Bool -> StateT CommandState TCM Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Bool -> StateT CommandState TCM Bool)
    -> TCMT IO Bool -> StateT CommandState TCM Bool
    forall a b. (a -> b) -> a -> b
    $ case Maybe CurrentFile
    cf of
        Maybe CurrentFile
    Nothing     -> Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        Just (CurrentFile AbsolutePath
    f [[Char]]
    _ ClockTime
    t) -> do
          ClockTime
    t' <- IO ClockTime -> TCM ClockTime
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO ClockTime -> TCM ClockTime) -> IO ClockTime -> TCM ClockTime
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO ClockTime
    getModificationTime ([Char] -> IO ClockTime) -> [Char] -> IO ClockTime
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> [Char]
    filePath AbsolutePath
    f
          if ClockTime
    t ClockTime -> ClockTime -> Bool
    forall a. Eq a => a -> a -> Bool
    == ClockTime
    t'
            then
              do
                Maybe TopLevelModuleName
    mm <- AbsolutePath -> TCM (Maybe TopLevelModuleName)
    forall (m :: * -> *).
    ReadTCState m =>
    AbsolutePath -> m (Maybe TopLevelModuleName)
    lookupModuleFromSource AbsolutePath
    f
                case Maybe TopLevelModuleName
    mm of
                  Maybe TopLevelModuleName
    Nothing -> Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False -- work-around for Issue1007
                  Just TopLevelModuleName
    m  -> Bool -> (ModuleInfo -> Bool) -> Maybe ModuleInfo -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False ([TCWarning] -> Bool
    forall a. Null a => a -> Bool
    null ([TCWarning] -> Bool)
    -> (ModuleInfo -> [TCWarning]) -> ModuleInfo -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleInfo -> [TCWarning]
    miWarnings) (Maybe ModuleInfo -> Bool)
    -> TCMT IO (Maybe ModuleInfo) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
    forall (m :: * -> *).
    ReadTCState m =>
    TopLevelModuleName -> m (Maybe ModuleInfo)
    getVisitedModule TopLevelModuleName
    m
            else
                Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

      Status -> CommandM Status
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Status -> CommandM Status) -> Status -> CommandM Status
    forall a b. (a -> b) -> a -> b
    $ Status :: Bool -> Bool -> Bool -> Status
    Status { sShowImplicitArguments :: Bool
    sShowImplicitArguments   = Bool
    showImpl,
                        sShowIrrelevantArguments :: Bool
    sShowIrrelevantArguments = Bool
    showIrr,
                        sChecked :: Bool
    sChecked                 = Bool
    checked }

    -- | Displays or updates status information.
    --
    --   Does not change the state.

    displayStatus :: CommandM ()
    displayStatus :: StateT CommandState TCM ()
    displayStatus =
      Response -> StateT CommandState TCM ()
    putResponse (Response -> StateT CommandState TCM ())
    -> (Status -> Response) -> Status -> StateT CommandState TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Status -> Response
    Resp_Status  (Status -> StateT CommandState TCM ())
    -> CommandM Status -> StateT CommandState TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< CommandM Status
    status

    -- | @display_info@ does what @'display_info'' False@ does, but
    --   additionally displays some status information (see 'status' and
    --   'displayStatus').

    display_info :: DisplayInfo -> CommandM ()
    display_info :: DisplayInfo -> StateT CommandState TCM ()
    display_info DisplayInfo
    info = do
      StateT CommandState TCM ()
    displayStatus
      Response -> StateT CommandState TCM ()
    putResponse (Response -> StateT CommandState TCM ())
    -> Response -> StateT CommandState TCM ()
    forall a b. (a -> b) -> a -> b
    $ DisplayInfo -> Response
    Resp_DisplayInfo DisplayInfo
    info

    -- | Parses and scope checks an expression (using the \"inside scope\"
    -- as the scope), performs the given command with the expression as
    -- input, and returns the result and the time it takes.

    parseAndDoAtToplevel
      :: (A.Expr -> TCM a)
         -- ^ The command to perform.
      -> String
         -- ^ The expression to parse.
      -> CommandM (Maybe CPUTime, a)
    parseAndDoAtToplevel :: forall a. (Expr -> TCM a) -> [Char] -> CommandM (Maybe CPUTime, a)
    parseAndDoAtToplevel Expr -> TCM a
    cmd [Char]
    s = do
      CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a)
    forall a. CommandM a -> CommandM a
    localStateCommandM (CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a))
    -> CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a)
    forall a b. (a -> b) -> a -> b
    $ do
        Expr
    e <- TCM Expr -> StateT CommandState TCM Expr
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Expr -> StateT CommandState TCM Expr)
    -> TCM Expr -> StateT CommandState TCM Expr
    forall a b. (a -> b) -> a -> b
    $ PM Expr -> TCM Expr
    forall a. PM a -> TCM a
    runPM (PM Expr -> TCM Expr) -> PM Expr -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ Parser Expr -> [Char] -> PM Expr
    forall a. Parser a -> [Char] -> PM a
    parse Parser Expr
    exprParser [Char]
    s
        CommandM a -> CommandM (Maybe CPUTime, a)
    forall a. CommandM a -> CommandM (Maybe CPUTime, a)
    maybeTimed (CommandM a -> CommandM (Maybe CPUTime, a))
    -> CommandM a -> CommandM (Maybe CPUTime, a)
    forall a b. (a -> b) -> a -> b
    $ CommandM a -> CommandM a
    forall a. CommandM a -> CommandM a
    atTopLevel (CommandM a -> CommandM a) -> CommandM a -> CommandM a
    forall a b. (a -> b) -> a -> b
    $ TCM a -> CommandM a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM a -> CommandM a) -> TCM a -> CommandM a
    forall a b. (a -> b) -> a -> b
    $
          Expr -> TCM a
    cmd (Expr -> TCM a) -> TCM Expr -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr -> ScopeM (AbsOfCon Expr)
    forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
    concreteToAbstract_ Expr
    e

    maybeTimed :: CommandM a -> CommandM (Maybe CPUTime, a)
    maybeTimed :: forall a. CommandM a -> CommandM (Maybe CPUTime, a)
    maybeTimed CommandM a
    work = do
      Bool
    doTime <- TCMT IO Bool -> StateT CommandState TCM Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Bool -> StateT CommandState TCM Bool)
    -> TCMT IO Bool -> StateT CommandState TCM Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> TCMT IO Bool
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m Bool
    hasVerbosity [Char]
    "profile.interactive" Int
    10
      if Bool -> Bool
    not Bool
    doTime
        then (Maybe CPUTime
    forall a. Maybe a
    Nothing,) (a -> (Maybe CPUTime, a))
    -> CommandM a -> CommandM (Maybe CPUTime, a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> CommandM a
    work
        else do
          (a
    r, CPUTime
    time) <- CommandM a -> StateT CommandState TCM (a, CPUTime)
    forall (m :: * -> *) a. MonadIO m => m a -> m (a, CPUTime)
    measureTime CommandM a
    work
          (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CPUTime -> Maybe CPUTime
    forall a. a -> Maybe a
    Just CPUTime
    time, a
    r)

    -- | Tell to highlight the code using the given highlighting
    -- info (unless it is @Nothing@).

    tellToUpdateHighlighting
      :: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource) -> IO [Response]
    tellToUpdateHighlighting :: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> IO [Response]
    tellToUpdateHighlighting Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    Nothing                = [Response] -> IO [Response]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
    tellToUpdateHighlighting (Just (HighlightingInfo
    info, HighlightingMethod
    method, ModuleToSource
    modFile)) =
      [Response] -> IO [Response]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [HighlightingInfo
    -> RemoveTokenBasedHighlighting
    -> HighlightingMethod
    -> ModuleToSource
    -> Response
    Resp_HighlightingInfo HighlightingInfo
    info RemoveTokenBasedHighlighting
    KeepHighlighting HighlightingMethod
    method ModuleToSource
    modFile]

    -- | Tells the Emacs mode to go to the first error position (if any).

    tellEmacsToJumpToError :: Range -> [Response]
    tellEmacsToJumpToError :: Range -> [Response]
    tellEmacsToJumpToError Range
    r =
      case Range -> Maybe (Position' (Maybe AbsolutePath))
    forall a. Range' a -> Maybe (Position' a)
    rStart Range
    r of
        Maybe (Position' (Maybe AbsolutePath))
    Nothing                                           -> []
        Just (Pn { srcFile :: forall a. Position' a -> a
    srcFile = Maybe AbsolutePath
    Strict.Nothing })            -> []
        Just (Pn { srcFile :: forall a. Position' a -> a
    srcFile = Strict.Just AbsolutePath
    f, posPos :: forall a. Position' a -> Int32
    posPos = Int32
    p }) ->
           [ [Char] -> Int32 -> Response
    Resp_JumpToError (AbsolutePath -> [Char]
    filePath AbsolutePath
    f) Int32
    p ]