# HG changeset patch
# User wenzelm
# Date 908556737 -7200
# Node ID f2c5354cd32f0e61bc89ffb78264383c0398d82d
# Parent  e2a2be6089b43287196ff763cd407208e3ded97e
tuned MLWorks options;
added print_depth;

diff -r e2a2be6089b4 -r f2c5354cd32f src/Pure/ML-Systems/mlworks.ML
--- a/src/Pure/ML-Systems/mlworks.ML	Fri Oct 16 18:50:50 1998 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML	Fri Oct 16 18:52:17 1998 +0200
@@ -18,9 +18,13 @@
 
 (* MLWorks parameters *)
 
-MLWorks.Internal.Runtime.Event.stack_overflow_handler
-  (fn () => MLWorks.Internal.Runtime.Memory.max_stack_blocks :=
-    ! MLWorks.Internal.Runtime.Memory.max_stack_blocks + 20);
+val _ =
+ (MLWorks.Internal.Runtime.Event.stack_overflow_handler
+    (fn () => MLWorks.Internal.Runtime.Memory.max_stack_blocks :=
+      ! MLWorks.Internal.Runtime.Memory.max_stack_blocks + 20);
+  MLWorks.Internal.Runtime.Memory.gc_message_level := 10;
+  (*Is this of any use at all?*)
+  Shell.Options.set (Shell.Options.ValuePrinter.showExnDetails, true));
 
 
 (* Poly/ML emulation *)
@@ -30,8 +34,8 @@
   | exit _ = OS.Process.exit OS.Process.failure;
 fun quit () = exit 0;
 
-(*n.a.*)
-fun print_depth n = ();
+(*limit the printing depth*)
+fun print_depth n = Shell.Options.set (Shell.Options.ValuePrinter.maximumDepth, n);
 
 (*interface for toplevel pretty printers, see also Pure/install_pp.ML*)
 (*n.a.*)