From 3d6cc2de08dc2f6c1be52cd218367b6bdb38ca50 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Sep 2020 15:53:23 -0700
Subject: [PATCH] feat: add `notFollowedByCategoryToken` parser

---
 src/Lean/Parser/Command.lean              |  9 -------
 src/Lean/Parser/Extension.lean            | 30 +++++++++++++++++++++++
 src/Lean/PrettyPrinter/Formatter.lean     |  1 +
 src/Lean/PrettyPrinter/Parenthesizer.lean |  1 +
 4 files changed, 32 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 111e918b9d..e9cdecb741 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -9,15 +9,6 @@ import Lean.Parser.Do
 namespace Lean
 namespace Parser
 
-@[init] def regBuiltinCommandParserAttr : IO Unit :=
-registerBuiltinParserAttribute `builtinCommandParser `command
-
-@[init] def regCommandParserAttribute : IO Unit :=
-registerBuiltinDynamicParserAttribute `commandParser `command
-
-@[inline] def commandParser (rbp : Nat := 0) : Parser :=
-categoryParser `command rbp
-
 /--
   Syntax quotation for terms and (lists of) commands. We prefer terms, so ambiguous quotations like
   `($x $y) will be parsed as an application, not two commands. Use `($x:command $y:command) instead.
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 39a0631a10..c3ac7351e1 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -463,5 +463,35 @@ registerBuiltinParserAttribute `builtinTermParser `term
 @[init] def regTermParserAttribute : IO Unit :=
 registerBuiltinDynamicParserAttribute `termParser `term
 
+-- declare `commandParser` to break cyclic dependency
+@[init] def regBuiltinCommandParserAttr : IO Unit :=
+registerBuiltinParserAttribute `builtinCommandParser `command
+
+@[init] def regCommandParserAttribute : IO Unit :=
+registerBuiltinDynamicParserAttribute `commandParser `command
+
+@[inline] def commandParser (rbp : Nat := 0) : Parser :=
+categoryParser `command rbp
+
+def notFollowedByCategoryTokenFn (catName : Name) : ParserFn :=
+fun ctx s =>
+  let categories := (parserExtension.getState ctx.env).categories;
+  match getCategory categories catName with
+  | none => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")
+  | some cat =>
+    let (s, stx) := peekToken ctx s;
+    match stx with
+    | some (Syntax.atom _ sym) =>
+      match cat.tables.leadingTable.find? (mkNameSimple sym) with
+      | some _ => s.mkError "notFollowedByCategoryToken"
+      | _      => s
+    | _ => s
+
+@[inline] def notFollowedByCategoryToken (catName : Name) : Parser :=
+{ fn := notFollowedByCategoryTokenFn catName }
+
+abbrev notFollowedByCommandToken : Parser :=
+notFollowedByCategoryToken `command
+
 end Parser
 end Lean
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index fa12c24cb3..066386f7ed 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -387,6 +387,7 @@ pushLine
 @[combinatorFormatter checkTailWs] def checkTailWs.formatter : Formatter := pure ()
 @[combinatorFormatter checkColGe] def checkColGe.formatter : Formatter := pure ()
 @[combinatorFormatter checkLineLe] def checkLineLe.formatter : Formatter := pure ()
+@[combinatorFormatter notFollowedByCategoryToken] def notFollowedByCategoryToken.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 3907531dd4..2b16fbb7ca 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.notFollowedByCategoryToken] def notFollowedByCategoryToken.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 ()