src/Pure/ML/ml_pretty.ML

--- a/src/Pure/ML/ml_pretty.ML	Thu Mar 17 12:32:12 2016 +0100
+++ b/src/Pure/ML/ml_pretty.ML	Thu Mar 17 13:44:18 2016 +0100
@@ -17,11 +17,15 @@
   val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
   val to_polyml: pretty -> PolyML.pretty
   val from_polyml: PolyML.pretty -> pretty
+  val get_print_depth: unit -> int
+  val print_depth: int -> unit
 end;
 
 structure ML_Pretty: ML_PRETTY =
 struct
 
+(* datatype pretty *)
+
 datatype pretty =
   Block of (string * string) * bool * FixedInt.int * pretty list |
   String of string * FixedInt.int |
@@ -81,4 +85,15 @@
           String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
   in convert "" end;
 
+
+(* default print depth *)
+
+local
+  val depth = Unsynchronized.ref 0;
+in
+  fun get_print_depth () = ! depth;
+  fun print_depth n = (depth := n; PolyML.print_depth n);
+  val _ = print_depth 10;
 end;
+
+end;