clarified modules;

--- a/src/Pure/ML/ml_options.ML	Thu Mar 17 12:32:12 2016 +0100
+++ b/src/Pure/ML/ml_options.ML	Thu Mar 17 13:44:18 2016 +0100
@@ -66,12 +66,12 @@
 (* print depth *)
 
 val print_depth_raw =
-  Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (get_default_print_depth ()));
+  Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (ML_Pretty.get_print_depth ()));
 val print_depth = Config.int print_depth_raw;
 
 fun get_print_depth () =
   (case Context.thread_data () of
-    NONE => get_default_print_depth ()
+    NONE => ML_Pretty.get_print_depth ()
   | SOME context => Config.get_generic context print_depth);
 
 fun get_print_depth_default default =

--- a/src/Pure/ML/ml_pretty.ML	Thu Mar 17 12:32:12 2016 +0100
+++ b/src/Pure/ML/ml_pretty.ML	Thu Mar 17 13:44:18 2016 +0100
@@ -17,11 +17,15 @@
   val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
   val to_polyml: pretty -> PolyML.pretty
   val from_polyml: PolyML.pretty -> pretty
+  val get_print_depth: unit -> int
+  val print_depth: int -> unit
 end;
 
 structure ML_Pretty: ML_PRETTY =
 struct
 
+(* datatype pretty *)
+
 datatype pretty =
   Block of (string * string) * bool * FixedInt.int * pretty list |
   String of string * FixedInt.int |
@@ -81,4 +85,15 @@
           String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
   in convert "" end;
 
+
+(* default print depth *)
+
+local
+  val depth = Unsynchronized.ref 0;
+in
+  fun get_print_depth () = ! depth;
+  fun print_depth n = (depth := n; PolyML.print_depth n);
+  val _ = print_depth 10;
 end;
+
+end;

--- a/src/Pure/ROOT.ML	Thu Mar 17 12:32:12 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 17 13:44:18 2016 +0100
@@ -56,14 +56,6 @@
 
 use "ML/ml_pretty.ML";
 
-local
-  val depth = Unsynchronized.ref 10;
-in
-  fun get_default_print_depth () = ! depth;
-  fun default_print_depth n = (depth := n; PolyML.print_depth n);
-  val _ = default_print_depth 10;
-end;
-
 val error_depth = PolyML.error_depth;
 
 

--- a/src/Pure/Tools/ml_process.scala	Thu Mar 17 12:32:12 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Thu Mar 17 13:44:18 2016 +0100
@@ -75,9 +75,9 @@
       else
         channel match {
           case None =>
-            List("(default_print_depth 10; Isabelle_Process.init_options ())")
+            List("(ML_Pretty.print_depth 10; Isabelle_Process.init_options ())")
           case Some(ch) =>
-            List("(default_print_depth 10; Isabelle_Process.init_protocol " +
+            List("(ML_Pretty.print_depth 10; Isabelle_Process.init_protocol " +
               ML_Syntax.print_string0(ch.server_name) + ")")
         }