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