src/Pure/ML/ml_print_depth0.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62900 c641bf9402fd
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@62878
     1
(*  Title:      Pure/ML/ml_print_depth0.ML
wenzelm@62878
     2
    Author:     Makarius
wenzelm@62878
     3
wenzelm@62878
     4
Print depth for ML toplevel pp -- global default (unsynchronized).
wenzelm@62878
     5
*)
wenzelm@62878
     6
wenzelm@62878
     7
signature ML_PRINT_DEPTH =
wenzelm@62878
     8
sig
wenzelm@62878
     9
  val set_print_depth: int -> unit
wenzelm@62878
    10
  val get_print_depth: unit -> int
wenzelm@62878
    11
end;
wenzelm@62878
    12
wenzelm@62878
    13
structure ML_Print_Depth: ML_PRINT_DEPTH =
wenzelm@62878
    14
struct
wenzelm@62878
    15
wenzelm@62878
    16
val depth = Unsynchronized.ref 0;
wenzelm@62878
    17
wenzelm@62878
    18
fun set_print_depth n = (depth := n; PolyML.print_depth n);
wenzelm@62878
    19
fun get_print_depth () = ! depth;
wenzelm@62878
    20
wenzelm@62878
    21
end;