--- 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);