From 2563d03ae2ccdf4ae76f28ccaf5dd246a0f9867f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 31 Aug 2020 14:21:08 -0700
Subject: [PATCH] feat: add `notFollowedBy`

---
 src/Lean/Parser/Basic.lean                | 15 +++++++++++++++
 src/Lean/PrettyPrinter/Formatter.lean     |  4 ++++
 src/Lean/PrettyPrinter/Parenthesizer.lean |  4 ++++
 3 files changed, 23 insertions(+)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 95c0c74dcd..efa1d81354 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -475,6 +475,21 @@ fun c s =>
 { info := p.info,
   fn   := lookaheadFn p.fn }
 
+@[inline] def notFollowedByFn (p : ParserFn) : ParserFn :=
+fun c s =>
+  let iniSz  := s.stackSize;
+  let iniPos := s.pos;
+  let s      := p c s;
+  if s.hasError then
+    s.restore iniSz iniPos
+  else
+    let s := s.restore iniSz iniPos;
+    s.mkError "notFollowedBy"
+
+@[inline] def notFollowedBy (p : Parser) : Parser :=
+{ info := p.info,
+  fn   := notFollowedByFn p.fn }
+
 @[specialize] partial def manyAux (p : ParserFn) : ParserFn
 | c, s =>
   let iniSz  := s.stackSize;
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 5def533fdb..cc98460872 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -232,6 +232,10 @@ p
 def lookahead.formatter (p : Formatter) : Formatter :=
 pure ()
 
+@[combinatorFormatter Lean.Parser.notFollowedBy]
+def notFollowedBy.formatter (p : Formatter) : Formatter :=
+pure ()
+
 @[combinatorFormatter Lean.Parser.andthen]
 def andthen.formatter (p1 p2 : Formatter) : Formatter :=
 p2 *> p1
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index ae7ad780a2..dd88158787 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -324,6 +324,10 @@ p
 def lookahead.parenthesizer (p : Parenthesizer) : Parenthesizer :=
 pure ()
 
+@[combinatorParenthesizer Lean.Parser.notFollowedBy]
+def notFollowedBy.parenthesizer (p : Parenthesizer) : Parenthesizer :=
+pure ()
+
 @[combinatorParenthesizer Lean.Parser.andthen]
 def andthen.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer :=
 p2 *> p1