Make do blocks require an expression
This makes for better error messages and fixes #1656.
Old message:
> :t do
When elaborating an application of constructor __infer:
INTERNAL ERROR: Invalid statement in do block
This is probably a bug, or a missing error message.
Please consider reporting at
https://github.com/idris-lang/Idris-dev/issues
New message:
> :t do
(input):1:6: error: unexpected
EOF, expected: ")",
do block expression,
end of "do", start of block
:t do<EOF>
commite6bbd1fe77f6ccf5566e5ce31dfc2f1ba066fe17
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateSat 18 Oct 2014, 11:48 (12 years ago)
parentb0e1ecf
src/Idris/ParseExpr.hs+1−1
@@ -1021,7 +1021,7 @@ DoBlock ::=
10211021doBlock :: SyntaxInfo -> IdrisParser PTerm
10221022doBlock syn
10231023 = do reserved "do"
1024− ds <- indentedBlock (do_ syn)
1024+ ds <- indentedBlock1 (do_ syn)
10251025 return (PDoBlock ds)
10261026 <?> "do block"
10271027