max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add checkLineLe parser

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-26 14:03:28 -07:00
parent 17e97baf8d
commit e31fd665f0
3 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Parser/Basic.lean
View file

@ -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 =>

1
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -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 ()

1
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -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 ()