@@ -24,6 +24,7 @@ import Idris.DSL
2424import Idris.Imports
2525import Idris.Delaborate
2626import Idris.Error
27+import Idris.Elab.Value
2728import Idris.ElabDecls
2829import Idris.ElabTerm
2930import Idris.Coverage
@@ -90,18 +91,21 @@ import System.IO
9091 ModuleHeader ::= 'module' Identifier_t ';'?;
9192@
9293-}
93−moduleHeader :: IdrisParser [String]
94−moduleHeader = try (do noDocCommentHere "Modules cannot have documentation comments"
94+moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])
95+moduleHeader = try (do docs <- optional docComment
96+ noArgs docs
9597 reserved "module"
9698 i <- identifier
9799 option ';' (lchar ';')
98− return (moduleName i))
100+ return (fmap fst docs, moduleName i))
99101 <|> try (do lchar '%'; reserved "unqualified"
100− return [])
101− <|> return (moduleName "Main")
102+ return (Nothing, []))
103+ <|> return (Nothing, moduleName "Main")
102104 where moduleName x = case span (/='.') x of
103105 (x, "") -> [x]
104106 (x, '.':y) -> x : moduleName y
107+ noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"
108+ noArgs _ = return ()
105109
106110{- | Parses an import statement
107111
@@ -1133,24 +1137,24 @@ parseTactic :: IState -> String -> Result PTactic
11331137parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
11341138
11351139-- | Parse module header and imports
1136−parseImports :: FilePath -> String -> Idris ([String], [(Bool, String, Maybe String, FC)], Maybe Delta)
1140+parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta)
11371141parseImports fname input
11381142 = do i <- getIState
11391143 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
11401144 Failure err -> fail (show err)
11411145 Success (x, i) -> do putIState i
11421146 return x
1143− where imports :: IdrisParser (([String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
1147+ where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
11441148 imports = do whiteSpace
1145− mname <- moduleHeader
1146− ps <- many import_
1147− mrk <- mark
1148− isEof <- lookAheadMatches eof
1149+ (mdoc, mname) <- moduleHeader
1150+ ps <- many import_
1151+ mrk <- mark
1152+ isEof <- lookAheadMatches eof
11491153 let mrk' = if isEof
11501154 then Nothing
11511155 else Just mrk
11521156 i <- get
1153− return ((mname, ps, mrk'), i)
1157+ return ((mdoc, mname, ps, mrk'), i)
11541158
11551159-- | There should be a better way of doing this...
11561160findFC :: Doc -> (FC, String)
@@ -1261,7 +1265,7 @@ loadSource lidr f toline
12611265 let def_total = default_total i
12621266 file_in <- runIO $ readFile f
12631267 file <- if lidr then tclift $ unlit f file_in else return file_in
1264− (mname, imports_in, pos) <- parseImports f file
1268+ (mdocs, mname, imports_in, pos) <- parseImports f file
12651269 ai <- getAutoImports
12661270 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
12671271 ids <- allImportDirs
@@ -1340,6 +1344,13 @@ loadSource lidr f toline
13401344 i <- getIState
13411345 addHides (hide_list i)
13421346
1347+ -- Save module documentation if applicable
1348+ i <- getIState
1349+ case mdocs of
1350+ Nothing -> return ()
1351+ Just docs -> addModDoc syntax mname docs
1352+
1353+
13431354 -- Finally, write an ibc if checking was successful
13441355 ok <- noErrors
13451356 when ok $
@@ -1364,6 +1375,17 @@ loadSource lidr f toline
13641375 PInstance _ _ _ _ _ _ _ _ -> r
13651376 _ -> x
13661377
1378+ addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1379+ addModDoc syn mname docs =
1380+ do ist <- getIState
1381+ docs' <- elabDocTerms recinfo (parsedDocs ist)
1382+ let modDocs' = addDef docName docs' (idris_moduledocs ist)
1383+ putIState ist { idris_moduledocs = modDocs' }
1384+ addIBC (IBCModDocs docName)
1385+ where
1386+ docName = NS modDocName (map T.pack (reverse mname))
1387+ parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1388+
13671389{- | Adds names to hide list -}
13681390addHides :: [(Name, Maybe Accessibility)] -> Idris ()
13691391addHides xs = do i <- getIState