# HG changeset patch
# User wenzelm
# Date 1372000460 -7200
# Node ID de8a85aad216ad31dfa17a6b978c8f88cdbd5943
# Parent  77075c576d4c749d3461e405785a57a855a6cd34
actually observe print_depth for outer term structure;

diff -r 77075c576d4c -r de8a85aad216 src/Pure/ML/install_pp_polyml.ML
--- a/src/Pure/ML/install_pp_polyml.ML	Sun Jun 23 16:47:45 2013 +0200
+++ b/src/Pure/ML/install_pp_polyml.ML	Sun Jun 23 17:14:20 2013 +0200
@@ -31,23 +31,23 @@
     val from_ML = Pretty.from_ML o pretty_ml;
     fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
     fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
-    fun prt_term parens dp (t as _ $ _) =
-          op :: (strip_comb t)
-          |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
-          |> Pretty.separate " $"
-          |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
-      | prt_term _ dp (Abs (x, T, body)) =
-          prt_apps "Abs"
-           [from_ML (prettyRepresentation (x, dp - 1)),
-            from_ML (prettyRepresentation (T, dp - 2)),
-            prt_term false (dp - 3) body]
-      | prt_term _ dp (Const const) =
-          prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
-      | prt_term _ dp (Free free) =
-          prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
-      | prt_term _ dp (Var var) =
-          prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
-      | prt_term _ dp (Bound i) =
-          prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
+    fun prt_term parens dp t =
+      if dp <= 0 then Pretty.str "..."
+      else
+        (case t of
+          _ $ _ =>
+            op :: (strip_comb t)
+            |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
+            |> Pretty.separate " $"
+            |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
+        | Abs (a, T, b) =>
+            prt_apps "Abs"
+             [from_ML (prettyRepresentation (a, dp - 1)),
+              from_ML (prettyRepresentation (T, dp - 2)),
+              prt_term false (dp - 3) b]
+        | Const const => prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
+        | Free free => prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
+        | Var var => prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
+        | Bound i => prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1))));
   in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);