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