src/Pure/ML-Systems/polyml.ML

--- a/src/Pure/ML-Systems/polyml.ML	Sat Aug 18 19:25:28 2007 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Sat Aug 18 21:27:52 2007 +0200
@@ -76,6 +76,14 @@
   pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
     fn () => brk (99999, 0), en);
 
+(*print depth*)
+local
+  val depth = ref 10;
+in
+  fun get_print_depth () = ! depth;
+  fun print_depth n = (depth := n; PolyML.print_depth n);
+end;
+
 
 (* ML command execution -- 'eval' *)