From 375e6232e08663ca6b77f1a31af5d2ebed53e311 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 25 Nov 2020 12:10:49 +0100
Subject: [PATCH] chore: introduce `doSeqItem` kind

---
 src/Lean/Parser/Do.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

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 :=