# HG changeset patch
# User wenzelm
# Date 1458319917 -3600
# Node ID 254582abf06719c3bd290c6067c0031302255ca9
# Parent  00aff1da05aee76b6446d858f0eee114ff03a9a7
clarified Pretty.T toplevel pp;

diff -r 00aff1da05ae -r 254582abf067 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Fri Mar 18 17:11:30 2016 +0100
+++ b/src/Pure/General/pretty.ML	Fri Mar 18 17:51:57 2016 +0100
@@ -72,7 +72,7 @@
   val block_enclose: T * T -> T list -> T
   val writeln_chunks: T list -> unit
   val writeln_chunks2: T list -> unit
-  val to_ML: T -> ML_Pretty.pretty
+  val to_ML: int -> T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
   val to_polyml: T -> PolyML.pretty
   val from_polyml: PolyML.pretty -> T
@@ -376,11 +376,12 @@
 
 (** toplevel pretty printing **)
 
-fun to_ML (Block (m, consistent, indent, prts, _)) =
-      ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map to_ML prts)
-  | to_ML (Break (force, wd, ind)) =
+fun to_ML 0 (Block _) = ML_Pretty.str "..."
+  | to_ML depth (Block (m, consistent, indent, prts, _)) =
+      ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map (to_ML (depth - 1)) prts)
+  | to_ML _ (Break (force, wd, ind)) =
       ML_Pretty.Break (force, FixedInt.fromInt wd, FixedInt.fromInt ind)
-  | to_ML (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len);
+  | to_ML _ (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len);
 
 fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
       make_block m consistent (FixedInt.toInt indent) (map from_ML prts)
@@ -388,12 +389,14 @@
       Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
   | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt len);
 
-val to_polyml = to_ML #> ML_Pretty.to_polyml;
+val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
 val from_polyml = ML_Pretty.from_polyml #> from_ML;
 
 end;
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn _: T => to_polyml (str "<pretty>"));
+val _ =
+  PolyML.addPrettyPrinter (fn depth => fn _ => ML_Pretty.to_polyml o to_ML (depth * 2 + 1) o quote);
+
 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
 
 end;
diff -r 00aff1da05ae -r 254582abf067 src/Pure/ML/ml_pp.ML
--- a/src/Pure/ML/ml_pp.ML	Fri Mar 18 17:11:30 2016 +0100
+++ b/src/Pure/ML/ml_pp.ML	Fri Mar 18 17:51:57 2016 +0100
@@ -104,7 +104,7 @@
 
 val _ =
   PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
-    ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf)));
+    ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));
 
 end;