From 12b267bd8cf0ef8d91f443059ea33bbae2e8b306 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 10 Nov 2022 10:22:20 +0100
Subject: [PATCH] refactor: `categoryParserOfStack` is dead

---
 src/Lean/Parser/Basic.lean                | 16 ----------------
 src/Lean/PrettyPrinter/Formatter.lean     |  6 ------
 src/Lean/PrettyPrinter/Parenthesizer.lean |  6 ------
 3 files changed, 28 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 1920115d34..571e5f6774 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1582,22 +1582,6 @@ def sepBy (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTraili
 def sepBy1 (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
   sepBy1NoAntiquot (sepByElemParser p sep) psep allowTrailingSep
 
-def categoryParserOfStackFn (offset : Nat) : ParserFn := fun ctx s =>
-  let stack := s.stxStack
-  if h : stack.size < offset + 1 then
-    s.mkUnexpectedError ("failed to determine parser category using syntax stack, stack is too small")
-  else
-    have : stack.size - (offset + 1) < stack.size := by
-      apply Nat.sub_lt <;> simp_all_arith
-      apply Nat.le_trans (m := offset + 1)
-      apply Nat.le_add_left; assumption
-    match stack[stack.size - (offset + 1)] with
-    | .ident _ _ catName _ => categoryParserFn catName ctx s
-    | _ => s.mkUnexpectedError ("failed to determine parser category using syntax stack, the specified element on the stack is not an identifier")
-
-def categoryParserOfStack (offset : Nat) (prec : Nat := 0) : Parser where
-  fn := adaptCacheableContextFn ({ · with prec }) (categoryParserOfStackFn offset)
-
 private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
   if s.stackSize == iniSz + 1 then s
   else s.mkNode nullKind iniSz -- throw error instead?
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 28b509c86b..5e19006272 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -267,12 +267,6 @@ def categoryParser.formatter (cat : Name) : Formatter := do
 def categoryFormatter (cat : Name) : Formatter :=
   fill <| indent <| categoryFormatterCore cat
 
-@[combinator_formatter categoryParserOfStack]
-def categoryParserOfStack.formatter (offset : Nat) : Formatter := do
-  let st ← get
-  let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
-  categoryParser.formatter stx.getId
-
 @[combinator_formatter parserOfStack]
 def parserOfStack.formatter (offset : Nat) (_prec : Nat := 0) : Formatter := do
   let st ← get
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index f57c80f170..4ae69811e2 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -324,12 +324,6 @@ def categoryParser.parenthesizer (cat : Name) (prec : Nat) : Parenthesizer := do
   -- In this case this node will never be parenthesized since we don't know which parentheses to use.
   | _    => parenthesizeCategoryCore cat prec
 
-@[combinator_parenthesizer categoryParserOfStack]
-def categoryParserOfStack.parenthesizer (offset : Nat) (prec : Nat) : Parenthesizer := do
-  let st ← get
-  let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
-  categoryParser.parenthesizer stx.getId prec
-
 @[combinator_parenthesizer parserOfStack]
 def parserOfStack.parenthesizer (offset : Nat) (_prec : Nat := 0) : Parenthesizer := do
   let st ← get