src/Pure/ML/ml_print_depth.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
parent 62878 1cec457e0a03
child 62900 c641bf9402fd
permissions -rw-r--r--
clarified modules;
tuned signature;
     1 (*  Title:      Pure/ML/ml_print_depth0.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   val get_print_depth_default: int -> int
    14 end;
    15 
    16 structure ML_Print_Depth: ML_PRINT_DEPTH =
    17 struct
    18 
    19 val set_print_depth = ML_Print_Depth.set_print_depth;
    20 
    21 val print_depth_raw =
    22   Config.declare ("ML_print_depth", @{here})
    23     (fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));
    24 
    25 val print_depth = Config.int print_depth_raw;
    26 
    27 fun get_print_depth () =
    28   (case Context.get_generic_context () of
    29     NONE => ML_Print_Depth.get_print_depth ()
    30   | SOME context => Config.get_generic context print_depth);
    31 
    32 fun get_print_depth_default default =
    33   (case Context.get_generic_context () of
    34     NONE => default
    35   | SOME context => Config.get_generic context print_depth);
    36 
    37 end;