feat: let/if indentation in do blocks

closes #1120

RELEASES.md

@@ -1,6 +1,8 @@
 Unreleased
 ---------
 
+* [`let/if` indentation in `do` blocks in now supported.](https://github.com/leanprover/lean4/issues/1120)
+
 * Updated Lake to v3.1.1. See the [v3.1.0 release note](https://github.com/leanprover/lake/releases/tag/v3.1.0) for detailed changes.
 
 * Add unnamed antiquotation `$_` for use in syntax quotation patterns.

src/Lean/Parser/Basic.lean

@@ -1491,6 +1491,14 @@ def anyOfFn : List Parser → ParserFn
     p.fn { c with savedPos? := s.pos } s
 }
 
+@[inline] def withPositionAfterLinebreak (p : Parser) : Parser := {
+  info := p.info
+  fn   := fun c s =>
+    let prev := s.stxStack.back
+    let c := if checkTailLinebreak prev then { c with savedPos? := s.pos } else c
+    p.fn c s
+}
+
 @[inline] def withoutPosition (p : Parser) : Parser := {
   info := p.info
   fn   := fun c s => p.fn { c with savedPos? := none } s

src/Lean/Parser/Do.lean

@@ -87,7 +87,7 @@ def doIfLetBind := leading_parser " ← " >> termParser
 def doIfLet     := leading_parser (withAnonymousAntiquot := false) "let " >> termParser >> (doIfLetPure <|> doIfLetBind)
 def doIfProp    := leading_parser (withAnonymousAntiquot := false) optIdent >> termParser
 def doIfCond    := withAntiquot (mkAntiquot "doIfCond" none (anonymous := false)) <| doIfLet <|> doIfProp
-@[builtinDoElemParser] def doIf := leading_parser withPosition $
+@[builtinDoElemParser] def doIf := leading_parser withPositionAfterLinebreak $
   "if " >> doIfCond >> " then " >> doSeq
   >> many (checkColGe "'else if' in 'do' must be indented" >> group (elseIf >> doIfCond >> " then " >> doSeq))
   >> optional (checkColGe "'else' in 'do' must be indented" >> " else " >> doSeq)

src/Lean/PrettyPrinter/Formatter.lean

@@ -449,6 +449,7 @@ def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
 @[combinatorFormatter Lean.Parser.sepBy1NoAntiquot] def sepBy1NoAntiquot.formatter := sepByNoAntiquot.formatter
 
 @[combinatorFormatter Lean.Parser.withPosition] def withPosition.formatter (p : Formatter) : Formatter := p
+@[combinatorFormatter Lean.Parser.withPositionAfterLinebreak] def withPositionAfterLinebreak.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.withForbidden] def withForbidden.formatter (_tk : Token) (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.withoutForbidden] def withoutForbidden.formatter (p : Formatter) : Formatter := p

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -464,6 +464,9 @@ def sepByNoAntiquot.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do
   -- We assume the formatter will indent syntax sufficiently such that parenthesizing a `withPosition` node is never necessary
   modify fun st => { st with contPrec := none }
   p
+@[combinatorParenthesizer Lean.Parser.withPositionAfterLinebreak] def withPositionAfterLinebreak.parenthesizer (p : Parenthesizer) : Parenthesizer :=
+  -- TODO: improve?
+  withPosition.parenthesizer p
 @[combinatorParenthesizer Lean.Parser.withoutPosition] def withoutPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := p
 @[combinatorParenthesizer Lean.Parser.withForbidden] def withForbidden.parenthesizer (_tk : Parser.Token) (p : Parenthesizer) : Parenthesizer := p
 @[combinatorParenthesizer Lean.Parser.withoutForbidden] def withoutForbidden.parenthesizer (p : Parenthesizer) : Parenthesizer := p

tests/lean/run/1120.lean

@@ -0,0 +1,6 @@
+example : Id Nat := do
+  let x ← if true then
+    pure 1
+  else
+    pure 2
+  pure x