# HG changeset patch
# User paulson
# Date 909161514 -7200
# Node ID 7ab9dd4a8ba6aa47394f7eafc076bbb31432bc07
# Parent  fb846bcb80cea66e9078e8485074a4f7810f0827
Warns when stack is extended; better decl of print_depth

diff -r fb846bcb80ce -r 7ab9dd4a8ba6 src/Pure/ML-Systems/mlworks.ML
--- a/src/Pure/ML-Systems/mlworks.ML	Fri Oct 23 18:48:59 1998 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML	Fri Oct 23 18:51:54 1998 +0200
@@ -19,9 +19,13 @@
 (* MLWorks parameters *)
 
 val _ =
- (MLWorks.Internal.Runtime.Event.stack_overflow_handler (fn () =>
+ (MLWorks.Internal.Runtime.Event.stack_overflow_handler 
+  (fn () =>
     let val max_stack = MLWorks.Internal.Runtime.Memory.max_stack_blocks
-    in max_stack := (! max_stack * 3) div 2 + 5 end);
+    in max_stack := (!max_stack * 3) div 2 + 5;
+       print ("#### Increasing stack to " ^ Int.toString (64 * !max_stack) ^
+	      "KB\n")
+    end);
   MLWorks.Internal.Runtime.Memory.gc_message_level := 10;
   (*Is this of any use at all?*)
   Shell.Options.set (Shell.Options.ValuePrinter.showExnDetails, true));
@@ -35,7 +39,11 @@
 fun quit () = exit 0;
 
 (*limit the printing depth*)
-fun print_depth n = Shell.Options.set (Shell.Options.ValuePrinter.maximumDepth, n);
+fun print_depth n = 
+    let open Shell.Options
+    in set (ValuePrinter.maximumDepth, n div 2);
+       set (ValuePrinter.maximumSeqSize, n)
+    end;
 
 (*interface for toplevel pretty printers, see also Pure/install_pp.ML*)
 (*n.a.*)