diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index a6a38c28f9..48efe40aa5 100644 --- a/src/Lean/Parser/Extra.lean +++ b/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] diff --git a/tests/lean/1606.lean b/tests/lean/1606.lean new file mode 100644 index 0000000000..f01e8acbce --- /dev/null +++ b/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 diff --git a/tests/lean/1606.lean.expected.out b/tests/lean/1606.lean.expected.out new file mode 100644 index 0000000000..a56bccaee0 --- /dev/null +++ b/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