From e31fd665f0368874c44ef5e88884695e38d4a52b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 26 Sep 2020 14:03:28 -0700 Subject: [PATCH] feat: add `checkLineLe` parser --- src/Lean/Parser/Basic.lean | 9 +++++++++ src/Lean/PrettyPrinter/Formatter.lean | 1 + src/Lean/PrettyPrinter/Parenthesizer.lean | 1 + 3 files changed, 11 insertions(+) diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 520114d327..2d2654c3e8 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1382,6 +1382,15 @@ fun c s => @[inline] def checkColGe (col : Nat) (errorMsg : String) : Parser := { fn := checkColGeFn col errorMsg } +@[inline] def checkLineLeFn (line : Nat) (errorMsg : String) : ParserFn := +fun c s => + let pos := c.fileMap.toPosition s.pos; + if pos.line ≤ line then s + else s.mkError errorMsg + +@[inline] def checkLineLe (line : Nat) (errorMsg : String) : Parser := +{ fn := checkLineLeFn line errorMsg } + @[inline] def withPosition (p : Position → Parser) : Parser := { info := (p { line := 1, column := 0 }).info, fn := fun c s => diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 43a303fa84..fa12c24cb3 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -386,6 +386,7 @@ pushLine @[combinatorFormatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter := pure () @[combinatorFormatter checkTailWs] def checkTailWs.formatter : Formatter := pure () @[combinatorFormatter checkColGe] def checkColGe.formatter : Formatter := pure () +@[combinatorFormatter checkLineLe] def checkLineLe.formatter : Formatter := pure () @[combinatorFormatter checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter := pure () @[combinatorFormatter Lean.Parser.checkInsideQuot] def checkInsideQuot.formatter : Formatter := pure () @[combinatorFormatter Lean.Parser.checkOutsideQuot] def checkOutsideQuot.formatter : Formatter := pure () diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 2a53f125fa..3907531dd4 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -447,6 +447,7 @@ p @[combinatorParenthesizer Lean.Parser.checkNoWsBefore] def checkNoWsBefore.parenthesizer : Parenthesizer := pure () @[combinatorParenthesizer Lean.Parser.checkTailWs] def checkTailWs.parenthesizer : Parenthesizer := pure () @[combinatorParenthesizer Lean.Parser.checkColGe] def checkColGe.parenthesizer : Parenthesizer := pure () +@[combinatorParenthesizer Lean.Parser.checkLineLe] def checkLineLe.parenthesizer : Parenthesizer := pure () @[combinatorParenthesizer Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.parenthesizer : Parenthesizer := pure () @[combinatorParenthesizer Lean.Parser.checkInsideQuot] def checkInsideQuot.parenthesizer : Parenthesizer := pure () @[combinatorParenthesizer Lean.Parser.checkOutsideQuot] def checkOutsideQuot.parenthesizer : Parenthesizer := pure ()