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