more accurate output: observe depth as in "prune" operation;

--- a/src/Pure/ML/ml_pretty.ML	Fri Sep 06 13:57:06 2024 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Fri Sep 06 14:34:07 2024 +0200
@@ -38,15 +38,18 @@
 val dots = str "...";
 
 fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
-  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
+  if depth = 0 then dots
+  else block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
 
 fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
-  let
-    fun elems _ [] = []
-      | elems 0 _ = [dots]
-      | elems d [x] = [pretty (x, d)]
-      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
-  in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
+  if depth = 0 then dots
+  else
+    let
+      fun elems _ [] = []
+        | elems 0 _ = [dots]
+        | elems d [x] = [pretty (x, d)]
+        | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
+    in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
 
 
 (* prune *)