module Agda.Interaction.Command.ShowScope where

import Agda.TypeChecking.Monad.Base (TCM)
import Agda.TypeChecking.Monad.State (getScope)
import Agda.Utils.Pretty (prettyShow)
import Data.ByteString (ByteString)

import Proof.Assistant.Helpers (toBS)

showScope :: TCM ByteString
showScope :: TCM ByteString
showScope = do
  ScopeInfo
scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> TCM ByteString)
-> (String -> ByteString) -> String -> TCM ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ByteString
toBS (String -> TCM ByteString) -> String -> TCM ByteString
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> String
forall a. Pretty a => a -> String
prettyShow ScopeInfo
scope