@@ -2,11 +2,13 @@
3module Idris.REPL.Browse (namespacesInNS, namesInNS) where
3module Idris.REPL.Browse (namespacesInNS, namesInNS) where
5+import Control.Monad (filterM)
5import Data.List (isSuffixOf, nub)
7import Data.List (isSuffixOf, nub)
6import Data.Maybe (mapMaybe)
8import Data.Maybe (mapMaybe)
7import qualified Data.Text as T (unpack)
9import qualified Data.Text as T (unpack)
9−import Idris.Core.Evaluate (ctxtAlist)
11+import Idris.Core.Evaluate (ctxtAlist, Accessibility(Hidden), lookupDefAccExact)
10import Idris.Core.TT (Name(..))
12import Idris.Core.TT (Name(..))
12import Idris.AbsSyntaxTree (Idris)
14import Idris.AbsSyntaxTree (Idris)
@@ -31,7 +33,12 @@ namespacesInNS ns = do let revNS = reverse ns
31namesInNS :: [String] -> Idris [Name]
33namesInNS :: [String] -> Idris [Name]
32namesInNS ns = do let revNS = reverse ns
34namesInNS ns = do let revNS = reverse ns
33 allNames <- fmap ctxtAlist getContext
35 allNames <- fmap ctxtAlist getContext
34− return [ n | (n, space) <- mapMaybe (getNS . fst) allNames
36+ let namesInSpace = [ n | (n, space) <- mapMaybe (getNS . fst) allNames
35− , revNS == space ]
37+ , revNS == space ]
38+ filterM accessible namesInSpace
36 where getNS n@(NS (UN n') namespace) = Just (n, (map T.unpack namespace))
39 where getNS n@(NS (UN n') namespace) = Just (n, (map T.unpack namespace))
37 getNS _ = Nothing
40 getNS _ = Nothing
41+ accessible n = do ctxt <- getContext
42+ case lookupDefAccExact n False ctxt of
43+ Just (_, Hidden ) -> return False