@@ -112,6 +112,8 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())
112 where inCommentChars :: MonadicParsing m => m ()
112 where inCommentChars :: MonadicParsing m => m ()
113 inCommentChars = try (string "-}" *> pure ())
113 inCommentChars = try (string "-}" *> pure ())
114 <|> try (multiLineComment *> inCommentChars)
114 <|> try (multiLineComment *> inCommentChars)
115+ <|> try (docComment '|' *> inCommentChars)
116+ <|> try (docComment '^' *> inCommentChars)
115 <|> try (skipSome (noneOf startEnd) *> inCommentChars)
117 <|> try (skipSome (noneOf startEnd) *> inCommentChars)
116 <|> oneOf startEnd *> inCommentChars
118 <|> oneOf startEnd *> inCommentChars
117 <?> "end of comment"
119 <?> "end of comment"
@@ -2560,7 +2562,7 @@ parseTactic :: IState -> String -> Result PTactic
2560parseTactic st = parseString (evalStateT (fullTactic defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2562parseTactic st = parseString (evalStateT (fullTactic defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2562-- | Parse module header and imports
2564-- | Parse module header and imports
2563−parseImports :: FilePath -> String -> Idris ([String], [String], Delta)
2565+parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
2564parseImports fname input
2566parseImports fname input
2565 = do i <- getIState
2567 = do i <- getIState
2566 case parseString (evalStateT imports i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
2568 case parseString (evalStateT imports i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
@@ -2568,18 +2570,22 @@ parseImports fname input
2568 Success (x, i) -> do -- Discard state updates (there should be
2570 Success (x, i) -> do -- Discard state updates (there should be
2569 -- none anyway)
2571 -- none anyway)
2570 return x
2572 return x
2571− where imports :: IdrisParser (([String], [String], Delta), IState)
2573+ where imports :: IdrisParser (([String], [String], Maybe Delta), IState)
2572 imports = do whiteSpace
2574 imports = do whiteSpace
2573 mname <- moduleHeader
2575 mname <- moduleHeader
2574 ps <- many import_
2576 ps <- many import_
2575 mrk <- mark
2577 mrk <- mark
2578+ isEof <- lookAheadMatches eof
2579+ let mrk' = if isEof
2576 i <- get
2582 i <- get
2577− return ((mname, ps, mrk), i)
2583+ return ((mname, ps, mrk'), i)
2580-- | A program is a list of declarations, possibly with associated
2586-- | A program is a list of declarations, possibly with associated
2581-- documentation strings.
2587-- documentation strings.
2582−parseProg :: SyntaxInfo -> FilePath -> String -> Delta ->
2588+parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
2583 Idris [PDecl]
2589 Idris [PDecl]
2584parseProg syn fname input mrk
2590parseProg syn fname input mrk
2585 = do i <- getIState
2591 = do i <- getIState
@@ -2593,10 +2599,13 @@ parseProg syn fname input mrk
2593 Success (x, i) -> do putIState i
2599 Success (x, i) -> do putIState i
2594 return $ collect x
2600 return $ collect x
2595 where mainProg :: IdrisParser ([PDecl], IState)
2601 where mainProg :: IdrisParser ([PDecl], IState)
2602+ mainProg = case mrk of
2603+ Nothing -> do i <- get; return ([], i)
2596− mainProg = do release mrk
2605+ release mrk
2597− ds <- prog syn
2606+ ds <- prog syn
2598− i' <- get
2607+ i' <- get
2599− return (ds, i')
2608+ return (ds, i')
2601-- | Collect 'PClauses' with the same function name
2610-- | Collect 'PClauses' with the same function name
2602collect :: [PDecl] -> [PDecl]
2611collect :: [PDecl] -> [PDecl]