From 9daed5e91d88bee46f07b485f89fd35eba7eee13 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 18 Mar 2021 06:43:03 -0700
Subject: [PATCH] chore: add `checkLinebreakBefore`

---
 src/Lean/Parser.lean                      |  1 +
 src/Lean/Parser/Basic.lean                | 14 ++++++++++++++
 src/Lean/PrettyPrinter/Formatter.lean     |  2 ++
 src/Lean/PrettyPrinter/Parenthesizer.lean |  2 ++
 4 files changed, 19 insertions(+)

diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean
index fdc04a5414..aa1c70fb4f 100644
--- a/src/Lean/Parser.lean
+++ b/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
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 3d329cdcda..ec3ec6a98d 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/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
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 9d03975006..7d2939feac 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/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
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index c5a6f64fca..707dd2c725 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/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