chore: add checkLinebreakBefore

src/Lean/Parser.lean

@@ -18,6 +18,7 @@ namespace Parser
 builtin_initialize
   registerAlias "ws" checkWsBefore
   registerAlias "noWs" checkNoWsBefore
+  registerAlias "linebreak" checkLinebreakBefore
   registerAlias "num" numLit
   registerAlias "str" strLit
   registerAlias "char" charLit

src/Lean/Parser/Basic.lean

@@ -1152,6 +1152,20 @@ def checkWsBefore (errorMsg : String := "space before") : Parser := {
   fn   := checkWsBeforeFn errorMsg
 }
 
+def checkTailLinebreak (prev : Syntax) : Bool :=
+  match prev.getTailInfo with
+  | SourceInfo.original _ _ trailing => trailing.contains '\n'
+  | _ => false
+
+def checkLinebreakBeforeFn (errorMsg : String) : ParserFn := fun c s =>
+  let prev := s.stxStack.back
+  if checkTailLinebreak prev then s else s.mkError errorMsg
+
+def checkLinebreakBefore (errorMsg : String := "line break") : Parser := {
+  info := epsilonInfo
+  fn   := checkLinebreakBeforeFn errorMsg
+}
+
 private def pickNonNone (stack : Array Syntax) : Syntax :=
   match stack.findRev? $ fun stx => !stx.isNone with
   | none => Syntax.missing

src/Lean/PrettyPrinter/Formatter.lean

@@ -426,6 +426,7 @@ def setExpected.formatter (expected : List String) (p : Formatter) : Formatter :
 @[combinatorFormatter Lean.Parser.checkNoWsBefore] def checkNoWsBefore.formatter : Formatter :=
   -- prevent automatic whitespace insertion
   modify fun st => { st with leadWord := "" }
+@[combinatorFormatter Lean.Parser.checkLinebreakBefore] def checkLinebreakBefore.formatter : Formatter := pure ()
 @[combinatorFormatter Lean.Parser.checkTailWs] def checkTailWs.formatter : Formatter := pure ()
 @[combinatorFormatter Lean.Parser.checkColGe] def checkColGe.formatter : Formatter := pure ()
 @[combinatorFormatter Lean.Parser.checkColGt] def checkColGt.formatter : Formatter := pure ()
@@ -464,6 +465,7 @@ instance : Coe (Formatter → Formatter → Formatter) FormatterAliasValue := {
 builtin_initialize
   registerAlias "ws" checkWsBefore.formatter
   registerAlias "noWs" checkNoWsBefore.formatter
+  registerAlias "linebreak" checkLinebreakBefore.formatter
   registerAlias "colGt" checkColGt.formatter
   registerAlias "colGe" checkColGe.formatter
   registerAlias "lookahead" lookahead.formatter

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -472,6 +472,7 @@ def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Par
 @[combinatorParenthesizer Lean.Parser.checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkNoWsBefore] def checkNoWsBefore.parenthesizer : Parenthesizer := pure ()
+@[combinatorParenthesizer Lean.Parser.checkLinebreakBefore] def checkLinebreakBefore.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkTailWs] def checkTailWs.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkColGe] def checkColGe.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkColGt] def checkColGt.parenthesizer : Parenthesizer := pure ()
@@ -512,6 +513,7 @@ instance : Coe (Parenthesizer → Parenthesizer → Parenthesizer) Parenthesizer
 builtin_initialize
   registerAlias "ws" checkWsBefore.parenthesizer
   registerAlias "noWs" checkNoWsBefore.parenthesizer
+  registerAlias "linebreak" checkLinebreakBefore.parenthesizer
   registerAlias "colGt" checkColGt.parenthesizer
   registerAlias "colGe" checkColGe.parenthesizer
   registerAlias "lookahead" lookahead.parenthesizer