From 14f2196d15c2acfe108d6be8b32884650062a1a5 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 8 Mar 2022 18:14:40 +0000
Subject: [PATCH] [ doc ] return module header docs

---
 src/Idris/Doc/String.idr      |  6 +++++-
 src/Idris/Parser.idr          |  3 ++-
 src/Idris/Syntax.idr          |  2 ++
 tests/Main.idr                |  2 +-
 tests/idris2/docs005/expected | 16 ++++++++++++++++
 tests/idris2/docs005/input    |  2 ++
 tests/idris2/docs005/run      |  3 +++
 7 files changed, 31 insertions(+), 3 deletions(-)
 create mode 100644 tests/idris2/docs005/expected
 create mode 100644 tests/idris2/docs005/input
 create mode 100755 tests/idris2/docs005/run

diff --git a/src/Idris/Doc/String.idr b/src/Idris/Doc/String.idr
index 46517ba9c..3c06c2bf1 100644
--- a/src/Idris/Doc/String.idr
+++ b/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} ->
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 68856adcd..69abc5bf6 100644
--- a/src/Idris/Parser.idr
+++ b/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 "|]")
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index eb6b5339d..5b17abaaf 100644
--- a/src/Idris/Syntax.idr
+++ b/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
diff --git a/tests/Main.idr b/tests/Main.idr
index b262ed238..5215b15e6 100644
--- a/tests/Main.idr
+++ b/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
diff --git a/tests/idris2/docs005/expected b/tests/idris2/docs005/expected
new file mode 100644
index 000000000..36f7747d3
--- /dev/null
+++ b/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!
diff --git a/tests/idris2/docs005/input b/tests/idris2/docs005/input
new file mode 100644
index 000000000..d7bb2ba77
--- /dev/null
+++ b/tests/idris2/docs005/input
@@ -0,0 +1,2 @@
+:module Data.Vect.AtIndex
+:doc module Data.Vect.AtIndex
diff --git a/tests/idris2/docs005/run b/tests/idris2/docs005/run
new file mode 100755
index 000000000..30854d92e
--- /dev/null
+++ b/tests/idris2/docs005/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner < input