From bd7bb6f5b5cb34c21905bdfe29cd2f561d2aa596 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 25 Nov 2020 09:52:46 +0100
Subject: [PATCH] fix: `do` formatting

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

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