src/Pure/ML/ml_print_depth.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 64556 851ae0e7b09c
child 69575 f77cc54f6d47
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Pure/ML/ml_print_depth.ML
     2     Author:     Makarius
     3 
     4 Print depth for ML toplevel pp: context option with global default.
     5 *)
     6 
     7 signature ML_PRINT_DEPTH =
     8 sig
     9   val set_print_depth: int -> unit
    10   val print_depth_raw: Config.raw
    11   val print_depth: int Config.T
    12   val get_print_depth: unit -> int
    13 end;
    14 
    15 structure ML_Print_Depth: ML_PRINT_DEPTH =
    16 struct
    17 
    18 val set_print_depth = ML_Print_Depth.set_print_depth;
    19 
    20 val print_depth_raw =
    21   Config.declare ("ML_print_depth", \<^here>)
    22     (fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));
    23 
    24 val print_depth = Config.int print_depth_raw;
    25 
    26 fun get_print_depth () =
    27   (case Context.get_generic_context () of
    28     NONE => ML_Print_Depth.get_print_depth ()
    29   | SOME context => Config.get_generic context print_depth);
    30 
    31 end;