git.iko.soy/Idris-dev
on master help sign in
Require content in tactic/proof blocks
c06badbEdwin Brady
src/Idris/ParseExpr.hs+2−2
compare with master
unifiedsplit
@@ -247,7 +247,7 @@ ProofExpr ::=
247-}
247-}
248proofExpr :: SyntaxInfo -> IdrisParser PTerm
248proofExpr :: SyntaxInfo -> IdrisParser PTerm
249proofExpr syn = do reserved "proof"
249proofExpr syn = do reserved "proof"
250− ts <- indentedBlock (tactic syn)
250+ ts <- indentedBlock1 (tactic syn)
251 return $ PProof ts
251 return $ PProof ts
252 <?> "proof block"
252 <?> "proof block"
253
253
@@ -260,7 +260,7 @@ TacticsExpr :=
260-}
260-}
261tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
261tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
262tacticsExpr syn = do reserved "tactics"
262tacticsExpr syn = do reserved "tactics"
263− ts <- indentedBlock (tactic syn)
263+ ts <- indentedBlock1 (tactic syn)
264 return $ PTactics ts
264 return $ PTactics ts
265 <?> "tactics block"
265 <?> "tactics block"
266
266