fix: trailing ';' at end of input
This commit is contained in:
parent
fbe1a94549
commit
39f8fd8eb9
2 changed files with 7 additions and 1 deletions
|
|
@ -78,7 +78,7 @@ withPosition fun pos₁ =>
|
|||
("; "
|
||||
-- check indentation
|
||||
>> checkColGe pos₁.column "do-elements must be indented"
|
||||
>> notFollowedByCommandToken)
|
||||
>> notFollowedByCommandToken >> notFollowedBy eoi)
|
||||
>> optional (try ("; " >> notFollowedByTermToken >> notFollowedBy (ident <|> numLit <|> strLit <|> charLit <|> nameLit)))
|
||||
def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
|
||||
def doSeq := doSeqBracketed <|> doSeqIndent
|
||||
|
|
|
|||
6
tests/lean/run/doTrailingAtEOI.lean
Normal file
6
tests/lean/run/doTrailingAtEOI.lean
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
new_frontend
|
||||
|
||||
|
||||
def f (x : Nat) : IO Nat := do
|
||||
IO.println x;
|
||||
pure x;
|
||||
Loading…
Add table
Reference in a new issue