module Agda.Interaction.Monad (IM, runIM, readline) where

import Control.Monad.Trans
import System.Console.Haskeline

import Agda.TypeChecking.Monad

-- | Line reader. The line reader history is not stored between
-- sessions.

readline :: String -> IM (Maybe String)
readline :: String -> IM (Maybe String)
readline String
s = InputT IO (Maybe String) -> IM (Maybe String)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (String -> InputT IO (Maybe String)
forall (m :: * -> *).
(MonadIO m, MonadMask m) =>
String -> InputT m (Maybe String)
getInputLine String
s)