From 5c74c408aed80e2661d033a352c6dd8385013945 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Oct 2020 07:43:30 -0700
Subject: [PATCH] chore: remove `nodeSepBy1Unbox` combinator

---
 src/Lean/Parser/Basic.lean                | 7 -------
 src/Lean/PrettyPrinter/Formatter.lean     | 8 --------
 src/Lean/PrettyPrinter/Parenthesizer.lean | 8 --------
 3 files changed, 23 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 6ade62be0a..633da987d2 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -604,13 +604,6 @@ fun c s =>
 @[inline] def many1Unbox (p : Parser) : Parser :=
 withResultOf (many1 p) fun stx => if stx.getNumArgs == 1 then stx.getArg 0 else stx
 
-@[inline] def nodeSepBy1Unbox (k : SyntaxNodeKind) (p sep : Parser) (allowTrailingSep := false) : Parser :=
-withResultOf (node k (sepBy1 p sep allowTrailingSep)) fun stx =>
-  if (stx.getArg 0).getNumArgs < 2 then
-    (stx.getArg 0).getArg 0
-  else
-    stx
-
 @[specialize] partial def satisfyFn (p : Char → Bool) (errorMsg : String := "unexpected character") : ParserFn
 | c, s =>
   let i := s.pos;
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index fda6806495..66507590fb 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -357,14 +357,6 @@ concatArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => if i % 2 == 0
 
 @[combinatorFormatter sepBy1] def sepBy1.formatter := sepBy.formatter
 
-@[combinatorFormatter Parser.nodeSepBy1Unbox]
-def nodeSepBy1Unbox.formatter (k : SyntaxNodeKind) (p sep : Formatter) : Formatter := do
-stx ← getCur;
-if stx.getKind == k then do
-  node.formatter k $ sepBy.formatter p sep
-else
-  p
-
 @[combinatorFormatter Lean.Parser.withPosition] def withPosition.formatter (p : Formatter) : Formatter := do
 p
 @[combinatorFormatter Lean.Parser.withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := do
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 3aa4c42e62..797edec6bf 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -422,14 +422,6 @@ visitArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => if i % 2 == 0
 
 @[combinatorParenthesizer Lean.Parser.sepBy1] def sepBy1.parenthesizer := sepBy.parenthesizer
 
-@[combinatorParenthesizer Lean.Parser.nodeSepBy1Unbox]
-def nodeSepBy1Unbox.parenthesizer (k : SyntaxNodeKind) (p pSep : Parenthesizer) : Parenthesizer := do
-stx ← getCur;
-if stx.getKind == k then
-  node.parenthesizer k $ sepBy.parenthesizer p pSep
-else
-  p
-
 @[combinatorParenthesizer Lean.Parser.withPosition] def withPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do
 p
 @[combinatorParenthesizer Lean.Parser.withoutPosition] def withoutPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do