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