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