src/Pure/ML-Systems/smlnj.ML
changeset 24329 f31594168d27
parent 24290 5607b8b752bb
child 24599 7b0ecf9a9055
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sat Aug 18 19:25:28 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sat Aug 18 21:27:52 2007 +0200
     1.3 @@ -43,10 +43,15 @@
     1.4  fun quit () = exit 0;
     1.5  
     1.6  (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
     1.7 -fun print_depth n =
     1.8 - (Control.Print.printDepth := (dest_int n) div 2;
     1.9 -  Control.Print.printLength := dest_int n);
    1.10 -
    1.11 +local
    1.12 +  val depth = ref 10;
    1.13 +in
    1.14 +  fun get_print_depth () = ! depth;
    1.15 +  fun print_depth n =
    1.16 +   (depth := n;
    1.17 +    Control.Print.printDepth := dest_int n div 2;
    1.18 +    Control.Print.printLength := dest_int n);
    1.19 +end;
    1.20  
    1.21  (* compiler-independent timing functions *)
    1.22