Add :browse

Lists all the names in a namespace with their types, and the first line
of their docstring if it exists

src/Core/Context.idr

@@ -863,6 +863,11 @@ HasNames Transform where
       = pure $ MkTransform !(resolved gam n) !(resolved gam env)
                            !(resolved gam lhs) !(resolved gam rhs)
 
+-- Return all the currently defined names
+export
+allNames : Context -> Core (List Name)
+allNames ctxt = traverse (full ctxt) $ map Resolved [1..nextEntry ctxt - 1]
+
 public export
 record Defs where
   constructor MkDefs

src/Idris/DocString.idr

@@ -63,7 +63,9 @@ getDocsFor fc n
 
     showTotal : Name -> Totality -> String
     showTotal n tot
-        = "\nTotality: " ++ show tot
+        = case isTerminating tot of
+               Unchecked => ""
+               _ => "\nTotality: " ++ show tot
 
     getConstructorDoc : Name -> Core (Maybe String)
     getConstructorDoc con
@@ -147,3 +149,44 @@ getDocsFor fc n
                               ++ "\n" ++ indent str
              extra <- getExtra n def
              pure (doc ++ extra)
+
+summarise : {auto c : Ref Ctxt Defs} ->
+            {auto s : Ref Syn SyntaxInfo} ->
+            Name -> Core String
+summarise n -- n is fully qualified
+    = do syn <- get Syn
+         defs <- get Ctxt
+         Just def <- lookupCtxtExact n (gamma defs)
+             | _ => pure ""
+         let doc = case lookupName n (docstrings syn) of
+                        [(_, doc)] => case lines doc of
+                                           (d :: _) => Just d
+                                           _ => Nothing
+                        _ => Nothing
+         ty <- normaliseHoles defs [] (type def)
+         pure (nameRoot n ++ " : " ++ show !(resugar [] ty) ++
+                  maybe "" (\d => "\n\t" ++ d) doc)
+         
+-- Display all the exported names in the given namespace
+export
+getContents : {auto c : Ref Ctxt Defs} ->
+              {auto s : Ref Syn SyntaxInfo} ->
+              List String -> Core (List String)
+getContents ns
+   = -- Get all the names, filter by any that match the given namespace
+     -- and are visible, then display with their type
+     do defs <- get Ctxt
+        ns <- allNames (gamma defs)
+        let allNs = filter inNS ns
+        allNs <- filterM (visible defs) allNs
+        traverse summarise (sort allNs)
+  where
+    visible : Defs -> Name -> Core Bool
+    visible defs n
+        = do Just def <- lookupCtxtExact n (gamma defs)
+                  | Nothing => pure False
+             pure (visibility def /= Private)
+
+    inNS : Name -> Bool
+    inNS (NS xns (UN _)) = xns == ns
+    inNS _ = False

src/Idris/Elab/Interface.idr

@@ -356,7 +356,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
                   Core (Name, List ImpClause)
     elabDefault tydecls (fc, opts, n, cs)
         = do -- orig <- branch
-             let dn_in = UN ("Default implementation of " ++ show n)
+             let dn_in = MN ("Default implementation of " ++ show n) 0
              dn <- inCurrentNS dn_in
 
              (rig, dty) <-

src/Idris/IDEMode/REPL.idr

@@ -16,6 +16,7 @@ import Core.TT
 import Core.Unify
 
 import Data.So
+import Data.Strings
 
 import Idris.Desugar
 import Idris.Error
@@ -188,8 +189,7 @@ process (CallsWho n)
     = do todoCmd "calls-who"
          pure $ NameList []
 process (BrowseNamespace ns)
-    = do todoCmd "browse-namespace"
-         pure $ NameList []
+    = replWrap $ Idris.REPL.process (Browse (reverse (split (=='.') ns)))
 process (NormaliseTerm tm)
     = do todoCmd "normalise-term"
          pure $ Term tm

src/Idris/Parser.idr

@@ -1923,6 +1923,7 @@ parserCommandsForHelp =
   , nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing "Show missing clauses"
   , nameArgCmd (ParseKeywordCmd "total") Total "Check the totality of a name"
   , nameArgCmd (ParseIdentCmd "doc") Doc "Show documentation for a name"
+  , moduleArgCmd (ParseIdentCmd "browse") Browse "Browse contents of a namespace"
   , numberArgCmd (ParseREPLCmd ["log", "logging"]) SetLog "Set logging level"
   , noArgCmd (ParseREPLCmd ["m", "metavars"]) Metavars "Show remaining proof obligations (metavariables or holes)"
   , noArgCmd (ParseREPLCmd ["version"]) ShowVersion "Display the Idris version"

src/Idris/REPL.idr

@@ -682,6 +682,9 @@ process (Total n)
 process (Doc n)
     = do doc <- getDocsFor replFC n
          pure $ Printed doc
+process (Browse ns)
+    = do doc <- getContents ns
+         pure $ Printed doc
 process (DebugInfo n)
     = do defs <- get Ctxt
          traverse_ showInfo !(lookupCtxtName n (gamma defs))

src/Idris/Syntax.idr

@@ -412,6 +412,7 @@ data REPLCmd : Type where
      Missing : Name -> REPLCmd
      Total : Name -> REPLCmd
      Doc : Name -> REPLCmd
+     Browse : List String -> REPLCmd
      SetLog : Nat -> REPLCmd
      Metavars : REPLCmd
      Editing : EditCmd -> REPLCmd

tests/Main.idr

@@ -46,7 +46,7 @@ idrisTests
        "coverage005", "coverage006", "coverage007", "coverage008",
        "coverage009", "coverage010",
        -- Documentation strings
-       "docs001",
+       "docs001", "docs002",
        -- Error messages
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",

tests/idris2/docs002/Doc.idr

@@ -0,0 +1,14 @@
+module Doc
+
+||| World!
+export
+world : Nat -> Nat
+world x = x*2
+
+nope : Nat
+nope = 0
+
+export
+||| Hello!
+hello : Int -> Int
+hello x = x*2

tests/idris2/docs002/expected

@@ -0,0 +1,6 @@
+1/1: Building Doc (Doc.idr)
+Doc> hello : Int -> Int
+	 Hello!
+world : Nat -> Nat
+	 World!
+Doc> Bye for now!

tests/idris2/docs002/input

@@ -0,0 +1,2 @@
+:browse Doc
+:q

tests/idris2/docs002/run

@@ -0,0 +1,3 @@
+$1 --no-banner Doc.idr < input
+
+rm -rf build