mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 11:05:17 +03:00
[ parser ] Make commitKeyword fail fatally
This commit is contained in:
parent
55926f30c5
commit
669f49e23e
@ -156,6 +156,7 @@ commitKeyword : OriginDesc -> IndentInfo -> String -> Rule ()
|
||||
commitKeyword fname indents req
|
||||
= do mustContinue indents (Just req)
|
||||
decoratedKeyword fname req
|
||||
<|> the (Rule ()) (fatalError ("Expected '" ++ req ++ "'"))
|
||||
mustContinue indents Nothing
|
||||
|
||||
commitSymbol : OriginDesc -> String -> Rule ()
|
||||
|
3
tests/idris2/perror016/ParseIf3.idr
Normal file
3
tests/idris2/perror016/ParseIf3.idr
Normal file
@ -0,0 +1,3 @@
|
||||
|
||||
test : Int -> Int
|
||||
test a = (if a < 0 the 0 else 5)
|
@ -1,16 +1,14 @@
|
||||
1/1: Building ParseIf (ParseIf.idr)
|
||||
Error: Couldn't parse any alternatives:
|
||||
1: Expected 'then'.
|
||||
Error: Expected 'then'.
|
||||
|
||||
ParseIf:3:26--3:30
|
||||
1 |
|
||||
2 | test : Int -> Int
|
||||
3 | test a = if a < 10 the 0 else a
|
||||
^^^^
|
||||
... (14 others)
|
||||
|
||||
1/1: Building ParseIf2 (ParseIf2.idr)
|
||||
Error: Couldn't parse any alternatives:
|
||||
1: Expected 'then'.
|
||||
Error: Expected 'then'.
|
||||
|
||||
ParseIf2:4:33--4:37
|
||||
1 |
|
||||
@ -18,4 +16,13 @@ ParseIf2:4:33--4:37
|
||||
3 | test a = if a < 10
|
||||
4 | then if a < 0 the 0 else 5
|
||||
^^^^
|
||||
... (28 others)
|
||||
|
||||
1/1: Building ParseIf3 (ParseIf3.idr)
|
||||
Error: Expected 'then'.
|
||||
|
||||
ParseIf3:3:26--3:30
|
||||
1 |
|
||||
2 | test : Int -> Int
|
||||
3 | test a = (if a < 0 the 0 else 5)
|
||||
^^^^
|
||||
|
||||
|
@ -2,3 +2,4 @@ rm -rf build
|
||||
|
||||
$1 --no-color --console-width 0 --check ParseIf.idr || true
|
||||
$1 --no-color --console-width 0 --check ParseIf2.idr || true
|
||||
$1 --no-color --console-width 0 --check ParseIf3.idr || true
|
||||
|
Loading…
Reference in New Issue
Block a user