@@ -45,7 +45,7 @@ import Paths_idris
4545import Util.DynamicLinker
4646import qualified Util.Pretty as P
4747
48−import Idris.Core.TT
48+import Idris.Core.TT as TT
4949import Idris.Core.Evaluate
5050
5151import Control.Applicative hiding (Const)
@@ -87,7 +87,7 @@ import System.IO
8787{- | Parses module definition
8888
8989@
90− ModuleHeader ::= 'module' Identifier_t ';'?;
90+ ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
9191@
9292-}
9393moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])
@@ -178,7 +178,8 @@ decl syn = do fc <- getFC
178178 <|> params syn
179179 <|> mutual syn
180180 <|> namespace syn
181− <|> (try (class_ syn) <|> instance_ syn)
181+ <|> class_ syn
182+ <|> instance_ syn
182183 <|> do d <- dsl syn; return [d]
183184 <|> directive syn
184185 <|> provider syn
@@ -347,13 +348,9 @@ fnDecl' :: SyntaxInfo -> IdrisParser PDecl
347348fnDecl' syn = checkFixity $
348349 do (doc, argDocs, fc, opts', n, acc) <- try (do
349350 pushIndent
350− (doc, argDocs) <- option noDocs docComment
351+ (doc, argDocs) <- docstring syn
351352 ist <- get
352− let doc' = annotCode (tryFullExpr syn ist) doc
353− argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
354− | (n, d) <- argDocs ]
355−
356− initOpts = if default_total ist
353+ let initOpts = if default_total ist
357354 then [TotalFn]
358355 else []
359356 opts <- fnOpts initOpts
@@ -363,7 +360,7 @@ fnDecl' syn = checkFixity $
363360 let n = expandNS syn n_in
364361 fc <- getFC
365362 lchar ':'
366− return (doc', argDocs', fc, opts', n, acc))
363+ return (doc, argDocs, fc, opts', n, acc))
367364 ty <- typeExpr (allowImp syn)
368365 terminator
369366 addAcc n acc
@@ -458,12 +455,10 @@ Postulate ::=
458455@
459456-}
460457postulate :: SyntaxInfo -> IdrisParser PDecl
461−postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment
462− ist <- get
463− let doc' = annotCode (tryFullExpr syn ist) doc
458+postulate syn = do doc <- try $ do (doc, _) <- docstring syn
464459 pushIndent
465460 reserved "postulate"
466− return doc'
461+ return doc
467462 ist <- get
468463 let initOpts = if default_total ist
469464 then [TotalFn]
@@ -586,7 +581,7 @@ ClassBlock ::=
586581classBlock :: SyntaxInfo -> IdrisParser [PDecl]
587582classBlock syn = do reserved "where"
588583 openBlock
589− ds <- many (try (notEndBlock >> instance_ syn) <|> fnDecl syn)
584+ ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)
590585 closeBlock
591586 return (concat ds)
592587 <?> "class block"
@@ -607,15 +602,14 @@ Class ::=
607602@
608603-}
609604class_ :: SyntaxInfo -> IdrisParser [PDecl]
610−class_ syn = do (doc, argDocs, acc) <- try (do
611− (doc, argDocs) <- option noDocs docComment
612− ist <- get
613− let doc' = annotCode (tryFullExpr syn ist) doc
614− argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
615− | (n, d) <- argDocs ]
616− acc <- optional accessibility
617− return (doc', argDocs', acc))
618− reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
605+class_ syn = do (doc, argDocs, acc)
606+ <- try (do (doc, argDocs) <- docstring syn
607+ acc <- optional accessibility
608+ reserved "class"
609+ return (doc, argDocs, acc))
610+ fc <- getFC
611+ cons <- constraintList syn
612+ n_in <- fnName
619613 let n = expandNS syn n_in
620614 cs <- many carg
621615 ds <- option [] (classBlock syn)
@@ -642,12 +636,9 @@ InstanceName ::= '[' Name ']';
642636@
643637-}
644638instance_ :: SyntaxInfo -> IdrisParser [PDecl]
645−instance_ syn = do doc <- try (do
646− (doc, _) <- option noDocs docComment
647− ist <- get
648− let doc' = annotCode (tryFullExpr syn ist) doc
649− return doc')
650− reserved "instance"; fc <- getFC
639+instance_ syn = do (doc, _)
640+ <- try (docstring syn <* reserved "instance")
641+ fc <- getFC
651642 en <- optional instanceName
652643 cs <- constraintList syn
653644 cn <- fnName
@@ -664,6 +655,18 @@ instance_ syn = do doc <- try (do
664655 <?> "instance name"
665656
666657
658+-- | Parse a docstring
659+docstring :: SyntaxInfo
660+ -> IdrisParser (Docstring (Either TT.Err PTerm),
661+ [(Name,Docstring (Either TT.Err PTerm))])
662+docstring syn = do (doc, argDocs) <- option noDocs docComment
663+ ist <- get
664+ let doc' = annotCode (tryFullExpr syn ist) doc
665+ argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
666+ | (n, d) <- argDocs ]
667+ return (doc', argDocs')
668+
669+
667670{- | Parses a using declaration list
668671
669672@