@@ -153,7 +153,7 @@ import_ = do fc <- getFC
153prog :: SyntaxInfo -> IdrisParser [PDecl]
153prog :: SyntaxInfo -> IdrisParser [PDecl]
154prog syn = do whiteSpace
154prog syn = do whiteSpace
155 decls <- many (decl syn)
155 decls <- many (decl syn)
156− let c = (concat decls)
156+ let c = concat decls
157 case maxline syn of
157 case maxline syn of
158 Nothing -> do notOpenBraces; eof
158 Nothing -> do notOpenBraces; eof
159 _ -> return ()
159 _ -> return ()
@@ -191,17 +191,27 @@ decl syn = try (externalDecl syn)
191internalDecl :: SyntaxInfo -> IdrisParser [PDecl]
191internalDecl :: SyntaxInfo -> IdrisParser [PDecl]
192internalDecl syn
192internalDecl syn
193 = do fc <- getFC
193 = do fc <- getFC
194− -- if we're after maxline, stop here
194+ -- if we're after maxline, stop at the next type declaration
195+ -- (so we get all cases of a definition to preserve totality
196+ -- results, in particular).
195 let continue = case maxline syn of
197 let continue = case maxline syn of
196 Nothing -> True
198 Nothing -> True
197 Just l -> if fst (fc_end fc) > l
199 Just l -> if fst (fc_end fc) > l
198 then mut_nesting syn /= 0
200 then mut_nesting syn /= 0
199 else True
201 else True
202+ -- What I'd really like to do here is explicitly save the
203+ -- current state, then if reading ahead finds we've passed
204+ -- the end of the definition, reset the state. But I've lost
205+ -- patience with trying to find out how to do that from the
206+ -- trifecta docs, so this does the job instead.
200− if continue then do notEndBlock
207+ if continue then
201− declBody
209+ declBody continue
210+ else try (do notEndBlock
202− else fail "End of readable input"
212+ <|> fail "End of readable input"
203− where declBody :: IdrisParser [PDecl]
213+ where declBody :: Bool -> IdrisParser [PDecl]
204− declBody = declBody'
214+ declBody b = declBody' b
205 <|> using_ syn
215 <|> using_ syn
206 <|> params syn
216 <|> params syn
207 <|> mutual syn
217 <|> mutual syn
@@ -214,11 +224,17 @@ internalDecl syn
214 <|> transform syn
224 <|> transform syn
215 <|> do import_; fail "imports must be at top of file"
225 <|> do import_; fail "imports must be at top of file"
216 <?> "declaration"
226 <?> "declaration"
217− declBody' :: IdrisParser [PDecl]
227+ declBody' :: Bool -> IdrisParser [PDecl]
218− declBody' = do d <- decl' syn
228+ declBody' cont = do d <- decl' syn
219− i <- get
229+ i <- get
220− let d' = fmap (debindApp syn . (desugar syn i)) d
230+ let d' = fmap (debindApp syn . (desugar syn i)) d
221− return [d']
232+ then return [d']
233+ else fail "End of readable input"
235+ -- Keep going while we're still parsing clauses
236+ continue False (PClauses _ _ _ _) = True
223{- | Parses a top-level declaration with possible syntax sugar
239{- | Parses a top-level declaration with possible syntax sugar