@@ -2562,7 +2562,7 @@ parseTactic :: IState -> String -> Result PTactic
2562parseTactic 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)
2564-- | Parse module header and imports
2564-- | Parse module header and imports
2565−parseImports :: FilePath -> String -> Idris ([String], [String], Delta)
2565+parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
2566parseImports fname input
2566parseImports fname input
2567 = do i <- getIState
2567 = do i <- getIState
2568 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
@@ -2570,18 +2570,22 @@ parseImports fname input
2570 Success (x, i) -> do -- Discard state updates (there should be
2570 Success (x, i) -> do -- Discard state updates (there should be
2571 -- none anyway)
2571 -- none anyway)
2572 return x
2572 return x
2573− where imports :: IdrisParser (([String], [String], Delta), IState)
2573+ where imports :: IdrisParser (([String], [String], Maybe Delta), IState)
2574 imports = do whiteSpace
2574 imports = do whiteSpace
2575 mname <- moduleHeader
2575 mname <- moduleHeader
2576 ps <- many import_
2576 ps <- many import_
2577 mrk <- mark
2577 mrk <- mark
2578+ isEof <- lookAheadMatches eof
2579+ let mrk' = if isEof
2578 i <- get
2582 i <- get
2579− return ((mname, ps, mrk), i)
2583+ return ((mname, ps, mrk'), i)
2582-- | A program is a list of declarations, possibly with associated
2586-- | A program is a list of declarations, possibly with associated
2583-- documentation strings.
2587-- documentation strings.
2584−parseProg :: SyntaxInfo -> FilePath -> String -> Delta ->
2588+parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
2585 Idris [PDecl]
2589 Idris [PDecl]
2586parseProg syn fname input mrk
2590parseProg syn fname input mrk
2587 = do i <- getIState
2591 = do i <- getIState
@@ -2595,10 +2599,13 @@ parseProg syn fname input mrk
2595 Success (x, i) -> do putIState i
2599 Success (x, i) -> do putIState i
2596 return $ collect x
2600 return $ collect x
2597 where mainProg :: IdrisParser ([PDecl], IState)
2601 where mainProg :: IdrisParser ([PDecl], IState)
2602+ mainProg = case mrk of
2603+ Nothing -> do i <- get; return ([], i)
2598− mainProg = do release mrk
2605+ release mrk
2599− ds <- prog syn
2606+ ds <- prog syn
2600− i' <- get
2607+ i' <- get
2601− return (ds, i')
2608+ return (ds, i')
2603-- | Collect 'PClauses' with the same function name
2610-- | Collect 'PClauses' with the same function name
2604collect :: [PDecl] -> [PDecl]
2611collect :: [PDecl] -> [PDecl]