[ doc ] return module header docs

src/Idris/Doc/String.idr

@@ -576,7 +576,11 @@ getDocs (APTerm ptm) = getDocsForPTerm ptm
 getDocs (Symbol k) = pure $ getDocsForSymbol k
 getDocs (Bracket IdiomBrackets) = pure "Idiom brackets (cf. manual)"
 getDocs (Keyword k) = pure $ getDocsForKeyword k
-
+getDocs (AModule mod) = do
+  syn  <- get Syn
+  let Just modDoc = lookup mod (modDocstrings syn)
+    | _ => throw (ModuleNotFound replFC mod)
+  pure (pretty modDoc)
 
 summarise : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->

src/Idris/Parser.idr

@@ -2061,7 +2061,8 @@ docArgCmd parseCmd command doc = (names, DocArg, doc, parse)
       symbol ":"
       runParseCmd parseCmd
       dir <- mustWork $
-        Keyword <$> anyKeyword
+        AModule <$ keyword "module" <*> moduleIdent -- must be before Keyword to not be captured
+        <|> Keyword <$> anyKeyword
         <|> Symbol <$> (anyReservedSymbol <* eoi
                        <|> parens (Virtual Interactive) anyReservedSymbol <* eoi)
         <|> Bracket <$> (IdiomBrackets <$ symbol "[|" <* symbol "|]")

src/Idris/Syntax.idr

@@ -599,6 +599,8 @@ data DocDirective : Type where
   Bracket : BracketType -> DocDirective
   ||| An arbitrary PTerm
   APTerm  : PTerm -> DocDirective
+  ||| A module name
+  AModule : ModuleIdent -> DocDirective
 
 public export
 data REPLCmd : Type where

tests/Main.idr

@@ -207,7 +207,7 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing
 idrisTests : TestPool
 idrisTests = MkTestPool "Misc" [] Nothing
        -- Documentation strings
-      ["docs001", "docs002", "docs003", "docs004",
+      ["docs001", "docs002", "docs003", "docs004", "docs005",
        -- Eta equality
        "eta001",
        -- Modules and imports

tests/idris2/docs005/expected

@@ -0,0 +1,16 @@
+Main> Imported module Data.Vect.AtIndex
+Main> Indexing Vectors.
+
+`Elem` proofs give existential quantification that a given element
+*is* in the list, but not where in the list it is!  Here we give a
+predicate that presents proof that a given index of a vector,
+given by a `Fin` instance, will return a certain element.
+
+Two decidable decision procedures are presented:
+
+1. Check that a given index points to the provided element in the
+   presented vector.
+
+2. Find the element at the given index in the presented vector.
+Main> 
+Bye for now!

tests/idris2/docs005/input

@@ -0,0 +1,2 @@
+:module Data.Vect.AtIndex
+:doc module Data.Vect.AtIndex

tests/idris2/docs005/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner < input