feat: use colEq in sepByIndent

src/Lean/Parser/Extra.lean

@@ -59,11 +59,11 @@ attribute [runBuiltinParserAttributeHooks]
 
 @[inline] def sepByIndent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
   let p := withAntiquotSpliceAndSuffix `sepBy p (symbol "*")
-  withPosition $ sepBy (checkColGe "irrelevant" >> p) sep (psep <|> checkLinebreakBefore >> pushNone) allowTrailingSep
+  withPosition $ sepBy (checkColGe "irrelevant" >> p) sep (psep <|> checkColEq "irrelevant" >> checkLinebreakBefore >> pushNone) allowTrailingSep
 
 @[inline] def sepBy1Indent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
   let p := withAntiquotSpliceAndSuffix `sepBy p (symbol "*")
-  withPosition $ sepBy1 (checkColGe "irrelevant" >> p) sep (psep <|> checkLinebreakBefore >> pushNone) allowTrailingSep
+  withPosition $ sepBy1 (checkColGe "irrelevant" >> p) sep (psep <|> checkColEq "irrelevant" >> checkLinebreakBefore >> pushNone) allowTrailingSep
 
 open PrettyPrinter Syntax.MonadTraverser Formatter in
 @[combinatorFormatter Lean.Parser.sepByIndent]

tests/lean/1606.lean

@@ -0,0 +1,22 @@
+example : True := by
+  skip
+    skip --< should complain about misleading indentation
+  trivial
+
+macro "frobnicate" : tactic => `(tactic| skip)
+
+example : True := by
+  conv =>
+    skip
+    frobnicate --< should not parse frobnicate as a tactic
+  trivial
+
+-- check error message without default handler for conv tactics
+declare_syntax_cat item
+syntax "valid_item" : item
+macro "block" "=>" sepByIndentSemicolon(item) : tactic => `(tactic| skip)
+
+example : True := by
+  block =>
+    valid_item
+    frobnicate --< should not parse frobnicate as a tactic

tests/lean/1606.lean.expected.out

@@ -0,0 +1,9 @@
+1606.lean:1:18-2:6: error: unsolved goals
+⊢ True
+1606.lean:3:4: error: expected command
+1606.lean:8:18-10:8: error: unsolved goals
+⊢ True
+1606.lean:11:4: error: expected command
+1606.lean:19:18-21:14: error: unsolved goals
+⊢ True
+1606.lean:22:4: error: expected command