From 57c8ab269b18395cb1f43843cc0efdeecd2ef82e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 24 Feb 2025 07:52:47 +0000
Subject: [PATCH] feat: allow line-wrapping when printing `DiscrTree.Key`s
 (#7200)

This PR allows the debug form of DiscrTree.Key to line-wrap.
---
 src/Lean/Meta/DiscrTree.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index ec38972a1e..57b229b4b3 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -96,13 +96,14 @@ where
     if args.isEmpty then
       return f
     else
-      let mut r := f
+      let mut r := m!""
       for arg in args do
-        r := r ++ m!" {arg}"
+        r := r ++ Format.line ++ arg
+      r := f ++ .nest 2 r
       if parenIfNonAtomic then
-        return m!"({r})"
+        return .paren r
       else
-        return r
+        return .group r
 
   go (parenIfNonAtomic := true) : StateRefT (List Key) CoreM MessageData := do
     let some key ← next? | return .nil