feat: optional ; at tacticSeq1Indented

src/Lean/Parser/Basic.lean

@@ -1420,8 +1420,11 @@ fun c s =>
 @[inline] def eoi : Parser :=
 { fn := eoiFn }
 
-@[inline] def many1Indent (p : Parser) (errorMsg : String) : Parser :=
-withPosition $ many1 (checkColGe errorMsg >> p)
+@[inline] def many1Indent (p : Parser) : Parser :=
+withPosition $ many1 (checkColGe "irrelevant" >> p)
+
+@[inline] def manyIndent (p : Parser) : Parser :=
+withPosition $ many (checkColGe "irrelevant" >> p)
 
 open Std (RBMap RBMap.empty)
 

src/Lean/Parser/Do.lean

@@ -21,25 +21,7 @@ namespace Term
 def leftArrow : Parser := unicodeSymbol " ← " " <- "
 @[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser
 
-def doSeqIndent :=
-withPosition $ many1 $
-  checkColGe "do-elements must be indented"
-  /-
-    We considered using `withPosition doElemParser` here instead of just `doElemParser` to make sure
-    the applications must be indented with respect to the current do-element.
-    Example:
-    ```
-    def foo : IO Nat := do
-    IO.println "hello";
-       List.forM xs
-     (fun x => IO.println x)
-    ```
-    The argument `(fun x => IO.println x)` is considered part of the application since it is
-    indented with respect to the first action.
-  -/
-  >> doElemParser
-  >> optional "; "
-
+def doSeqIndent    := many1Indent $ doElemParser >> optional "; "
 def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
 def doSeq          := doSeqBracketed <|> doSeqIndent
 

src/Lean/Parser/Tactic.lean

@@ -25,11 +25,11 @@ fun c s =>
 
 def ident' : Parser := ident <|> underscore
 
-@[builtinTacticParser] def «intro»      := parser! nonReservedSymbol "intro " >> notFollowedBy "|" >> many (termParser maxPrec)
-@[builtinTacticParser] def «intros»     := parser! nonReservedSymbol "intros " >> many ident'
-@[builtinTacticParser] def «revert»     := parser! nonReservedSymbol "revert " >> many1 ident
-@[builtinTacticParser] def «clear»      := parser! nonReservedSymbol "clear " >> many1 ident
-@[builtinTacticParser] def «subst»      := parser! nonReservedSymbol "subst " >> many1 ident
+@[builtinTacticParser] def «intro»      := parser! nonReservedSymbol "intro " >> notFollowedBy "|" >> manyIndent (termParser maxPrec)
+@[builtinTacticParser] def «intros»     := parser! nonReservedSymbol "intros " >> manyIndent ident'
+@[builtinTacticParser] def «revert»     := parser! nonReservedSymbol "revert " >> many1Indent ident
+@[builtinTacticParser] def «clear»      := parser! nonReservedSymbol "clear " >> many1Indent ident
+@[builtinTacticParser] def «subst»      := parser! nonReservedSymbol "subst " >> many1Indent ident
 @[builtinTacticParser] def «assumption» := parser! nonReservedSymbol "assumption"
 @[builtinTacticParser] def «apply»      := parser! nonReservedSymbol "apply " >> termParser
 @[builtinTacticParser] def «exact»      := parser! nonReservedSymbol "exact " >> termParser

src/Lean/Parser/Term.lean

@@ -22,8 +22,7 @@ categoryParser `tactic rbp
 namespace Tactic
 
 def tacticSeq1Indented : Parser :=
-parser! withPosition $
-  sepBy1 tacticParser (try ("; " >>  checkColGe "tatic must be indented"))
+parser! many1Indent $ tacticParser >> optional "; "
 def tacticSeqBracketed : Parser :=
 parser! "{" >> sepBy tacticParser "; " true >> "}"
 def tacticSeq :=