1(*  Title:      Pure/ML/ml_print_depth.ML
2    Author:     Makarius
3
4Print depth for ML toplevel pp: context option with global default.
5*)
6
7signature ML_PRINT_DEPTH =
8sig
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
13end;
14
15structure ML_Print_Depth: ML_PRINT_DEPTH =
16struct
17
18val set_print_depth = ML_Print_Depth.set_print_depth;
19
20val print_depth_raw =
21  Config.declare ("ML_print_depth", \<^here>)
22    (fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));
23
24val print_depth = Config.int print_depth_raw;
25
26fun 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
31end;
32