diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index 1fecc84e1f..fe3fb04022 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -18,8 +18,9 @@ namespace Term def leftArrow : Parser := unicodeSymbol " ← " " <- " @[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser -def doSeqIndent := parser! many1Indent $ group (ppLine >> doElemParser >> optional "; ") -def doSeqBracketed := parser! "{" >> withoutPosition (many1 (group (ppLine >> doElemParser >> optional "; "))) >> ppLine >> "}" +def doSeqItem := parser! ppLine >> doElemParser >> optional "; " +def doSeqIndent := parser! many1Indent doSeqItem +def doSeqBracketed := parser! "{" >> withoutPosition (many1 doSeqItem) >> ppLine >> "}" def doSeq := doSeqBracketed <|> doSeqIndent def notFollowedByRedefinedTermToken :=