From 0880332761b4349b37469cef40ee90e45ffe8d71 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 22 Dec 2019 08:23:13 -0800
Subject: [PATCH] feat: add `maxDepth` option to `formatStx`

---
 src/Init/Lean/Syntax.lean | 27 +++++++++++++++++++--------
 1 file changed, 19 insertions(+), 8 deletions(-)

diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean
index 1e053ac173..b028410365 100644
--- a/src/Init/Lean/Syntax.lean
+++ b/src/Init/Lean/Syntax.lean
@@ -295,18 +295,29 @@ partial def reprint : Syntax → Option String
 
 open Lean.Format
 
-protected partial def formatStx : Syntax → Format
-| atom info val     => format $ repr val
-| ident _ _ val pre => format "`" ++ format val
-| node kind args    =>
+partial def formatStxAux (maxDepth : Option Nat) : Nat → Syntax → Format
+| _,     atom info val     => format $ repr val
+| _,     ident _ _ val pre => format "`" ++ format val
+| _,     missing           => "<missing>"
+| depth, node kind args    =>
+  let depth := depth + 1;
   if kind == `Lean.Parser.noKind then
-    sbracket $ joinSep (args.toList.map formatStx) line
+    sbracket $
+      if depth > maxDepth.getD depth then
+        ".."
+      else
+        joinSep (args.toList.map (formatStxAux depth)) line
   else
     let shorterName := kind.replacePrefix `Lean.Parser Name.anonymous;
-    paren $ joinSep ((format shorterName) :: args.toList.map formatStx) line
-| missing => "<missing>"
+    let header      := format shorterName;
+    let body : List Format :=
+      if depth > maxDepth.getD depth then [".."] else args.toList.map (formatStxAux depth);
+    paren $ joinSep (header :: body) line
 
-instance : HasFormat (Syntax)   := ⟨Syntax.formatStx⟩
+def formatStx (stx : Syntax) (maxDepth : Option Nat := none) : Format :=
+formatStxAux maxDepth 0 stx
+
+instance : HasFormat (Syntax)   := ⟨formatStx⟩
 instance : HasToString (Syntax) := ⟨toString ∘ format⟩
 
 end Syntax