@@ -112,6 +112,8 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())
112112 where inCommentChars :: MonadicParsing m => m ()
113113 inCommentChars = try (string "-}" *> pure ())
114114 <|> try (multiLineComment *> inCommentChars)
115+ <|> try (docComment '|' *> inCommentChars)
116+ <|> try (docComment '^' *> inCommentChars)
115117 <|> try (skipSome (noneOf startEnd) *> inCommentChars)
116118 <|> oneOf startEnd *> inCommentChars
117119 <?> "end of comment"
@@ -2560,7 +2562,7 @@ parseTactic :: IState -> String -> Result PTactic
25602562parseTactic st = parseString (evalStateT (fullTactic defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
25612563
25622564-- | Parse module header and imports
2563−parseImports :: FilePath -> String -> Idris ([String], [String], Delta)
2565+parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
25642566parseImports fname input
25652567 = do i <- getIState
25662568 case parseString (evalStateT imports i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
@@ -2568,18 +2570,22 @@ parseImports fname input
25682570 Success (x, i) -> do -- Discard state updates (there should be
25692571 -- none anyway)
25702572 return x
2571− where imports :: IdrisParser (([String], [String], Delta), IState)
2573+ where imports :: IdrisParser (([String], [String], Maybe Delta), IState)
25722574 imports = do whiteSpace
25732575 mname <- moduleHeader
25742576 ps <- many import_
25752577 mrk <- mark
2578+ isEof <- lookAheadMatches eof
2579+ let mrk' = if isEof
2580+ then Nothing
2581+ else Just mrk
25762582 i <- get
2577− return ((mname, ps, mrk), i)
2583+ return ((mname, ps, mrk'), i)
25782584
25792585
25802586-- | A program is a list of declarations, possibly with associated
25812587-- documentation strings.
2582−parseProg :: SyntaxInfo -> FilePath -> String -> Delta ->
2588+parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
25832589 Idris [PDecl]
25842590parseProg syn fname input mrk
25852591 = do i <- getIState
@@ -2593,10 +2599,13 @@ parseProg syn fname input mrk
25932599 Success (x, i) -> do putIState i
25942600 return $ collect x
25952601 where mainProg :: IdrisParser ([PDecl], IState)
2596− mainProg = do release mrk
2597− ds <- prog syn
2598− i' <- get
2599− return (ds, i')
2602+ mainProg = case mrk of
2603+ Nothing -> do i <- get; return ([], i)
2604+ Just mrk -> do
2605+ release mrk
2606+ ds <- prog syn
2607+ i' <- get
2608+ return (ds, i')
26002609
26012610-- | Collect 'PClauses' with the same function name
26022611collect :: [PDecl] -> [PDecl]