src/Pure/ML/ml_print_depth.ML

simplified default print_depth: context is usually available, in contrast to 0d295e339f52;

(*  Title:      Pure/ML/ml_print_depth0.ML
    Author:     Makarius

Print depth for ML toplevel pp: context option with global default.
*)

signature ML_PRINT_DEPTH =
sig
  val set_print_depth: int -> unit
  val print_depth_raw: Config.raw
  val print_depth: int Config.T
  val get_print_depth: unit -> int
end;

structure ML_Print_Depth: ML_PRINT_DEPTH =
struct

val set_print_depth = ML_Print_Depth.set_print_depth;

val print_depth_raw =
  Config.declare ("ML_print_depth", @{here})
    (fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));

val print_depth = Config.int print_depth_raw;

fun get_print_depth () =
  (case Context.get_generic_context () of
    NONE => ML_Print_Depth.get_print_depth ()
  | SOME context => Config.get_generic context print_depth);

end;