1(*  Title:      Pure/ML/ml_print_depth0.ML
2    Author:     Makarius
3
4Print depth for ML toplevel pp -- global default (unsynchronized).
5*)
6
7signature ML_PRINT_DEPTH =
8sig
9  val set_print_depth: int -> unit
10  val get_print_depth: unit -> int
11end;
12
13structure ML_Print_Depth: ML_PRINT_DEPTH =
14struct
15
16val depth = Unsynchronized.ref 0;
17
18fun set_print_depth n = (depth := n; PolyML.print_depth n);
19fun get_print_depth () = ! depth;
20
21end;
22