src/Pure/ML/ml_print_depth.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_print_depth.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -0,0 +1,37 @@
+(*  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
+  val get_print_depth_default: int -> 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.thread_data () of
+    NONE => ML_Print_Depth.get_print_depth ()
+  | SOME context => Config.get_generic context print_depth);
+
+fun get_print_depth_default default =
+  (case Context.thread_data () of
+    NONE => default
+  | SOME context => Config.get_generic context print_depth);
+
+end;