clarified modules -- simplified bootstrap;

--- a/src/Pure/Isar/attrib.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -515,11 +515,11 @@
   register_config Name_Space.names_long_raw #>
   register_config Name_Space.names_short_raw #>
   register_config Name_Space.names_unique_raw #>
+  register_config ML_Print_Depth.print_depth_raw #>
   register_config ML_Options.source_trace_raw #>
   register_config ML_Options.exception_trace_raw #>
   register_config ML_Options.exception_debugger_raw #>
   register_config ML_Options.debugger_raw #>
-  register_config ML_Options.print_depth_raw #>
   register_config Proof_Context.show_abbrevs_raw #>
   register_config Goal_Display.goals_limit_raw #>
   register_config Goal_Display.show_main_goal_raw #>

--- a/src/Pure/Isar/runtime.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/Isar/runtime.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -43,7 +43,7 @@
 fun pretty_exn (exn: exn) =
   Pretty.from_ML
     (ML_Pretty.from_polyml
-      (ML_system_pretty (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
+      (ML_system_pretty (exn, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()))));
 
 
 (* exn_context *)

--- a/src/Pure/ML/ml_compiler.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -199,7 +199,7 @@
 
     (* results *)
 
-    val depth = FixedInt.fromInt (ML_Options.get_print_depth ());
+    val depth = FixedInt.fromInt (ML_Print_Depth.get_print_depth ());
 
     fun apply_result {fixes, types, signatures, structures, functors, values} =
       let
@@ -258,7 +258,7 @@
       PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
       PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
       PolyML.Compiler.CPFileName location_props,
-      PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
+      PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
       PolyML.Compiler.CPPrintInAlphabeticalOrder false,
       PolyML.Compiler.CPDebug debug];

--- a/src/Pure/ML/ml_context.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -118,8 +118,8 @@
      \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
      " (Context.the_local_context ());\n\
      \val ML_print_depth =\n\
-     \  let val default = ML_Options.get_print_depth ()\n\
-     \  in fn () => ML_Options.get_print_depth_default default end;\n"),
+     \  let val default = ML_Print_Depth.get_print_depth ()\n\
+     \  in fn () => ML_Print_Depth.get_print_depth_default default end;\n"),
    ML_Lex.tokenize "end;");
 
 fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end");

--- a/src/Pure/ML/ml_options.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/ML/ml_options.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -17,10 +17,6 @@
   val debugger_raw: Config.raw
   val debugger: bool Config.T
   val debugger_enabled: Context.generic option -> bool
-  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_Options: ML_OPTIONS =
@@ -62,21 +58,4 @@
       (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false)
   | debugger_enabled (SOME context) = Config.get_generic context debugger;
 
-
-(* print depth *)
-
-val print_depth_raw =
-  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 => ML_Pretty.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;

--- a/src/Pure/ML/ml_pretty.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -19,8 +19,6 @@
     'a list * FixedInt.int -> pretty
   val to_polyml: pretty -> PolyML_Pretty.pretty
   val from_polyml: PolyML_Pretty.pretty -> pretty
-  val get_print_depth: unit -> int
-  val print_depth: int -> unit
   val format_polyml: int -> PolyML_Pretty.pretty -> string
   val format: int -> pretty -> string
   val make_string_fn: string -> string
@@ -91,16 +89,6 @@
   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);
-end;
-
-
 (* format *)
 
 fun format_polyml margin prt =
@@ -123,8 +111,8 @@
   if local_env <> "" then
     pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()"))
   else if List.exists (fn (a, _) => a = "Pretty") (#allStruct ML_Name_Space.global ()) then
-    pretty_string_of (pretty_value "ML_Pretty.get_print_depth ()")
-  else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Pretty.get_print_depth ()" ^ "))";
+    pretty_string_of (pretty_value "ML_Print_Depth.get_print_depth ()")
+  else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Print_Depth.get_print_depth ()" ^ "))";
 
 end;
 

--- /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;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_print_depth0.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -0,0 +1,23 @@
+(*  Title:      Pure/ML/ml_print_depth0.ML
+    Author:     Makarius
+
+Print depth for ML toplevel pp -- global default (unsynchronized).
+*)
+
+signature ML_PRINT_DEPTH =
+sig
+  val set_print_depth: int -> unit
+  val get_print_depth: unit -> int
+  val get_print_depth_default: int -> int
+end;
+
+structure ML_Print_Depth: ML_PRINT_DEPTH =
+struct
+
+val depth = Unsynchronized.ref 0;
+
+fun set_print_depth n = (depth := n; PolyML.print_depth n);
+fun get_print_depth () = ! depth;
+fun get_print_depth_default _ = ! depth;
+
+end;

--- a/src/Pure/ROOT.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/ROOT.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -23,6 +23,7 @@
 
 use "ML/ml_heap.ML";
 use "ML/ml_profiling.ML";
+use "ML/ml_print_depth0.ML";
 use "ML/ml_pretty.ML";
 use "ML/ml_compiler0.ML";
 use_no_debug "ML/ml_debugger.ML";
@@ -185,6 +186,7 @@
 use "ML/ml_syntax.ML";
 use "ML/ml_env.ML";
 use "ML/ml_options.ML";
+use "ML/ml_print_depth.ML";
 use_no_debug "ML/exn_debugger.ML";
 use_no_debug "Isar/runtime.ML";
 use "PIDE/execution.ML";

--- a/src/Pure/System/isabelle_process.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -209,7 +209,7 @@
 (* init options *)
 
 fun init_options () =
- (ML_Pretty.print_depth (Options.default_int "ML_print_depth");
+ (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
   Future.ML_statistics := Options.default_bool "ML_statistics";
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");

--- a/src/Pure/System/options.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/System/options.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -222,6 +222,6 @@
       end);
 
 val _ = load_default ();
-val _ = ML_Pretty.print_depth (default_int "ML_print_depth");
+val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth");
 
 end;

--- a/src/Pure/Tools/debugger.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/Tools/debugger.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -190,7 +190,7 @@
 
     fun print x =
       Pretty.from_polyml
-        (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
+        (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), space));
     fun print_all () =
       #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
       |> sort_by #1 |> map (Pretty.item o single o print o #2)