# HG changeset patch
# User wenzelm
# Date 1458992111 -3600
# Node ID 22a17cec2efe03fb6d3db4c914f38131f3a07bc8
# Parent  09df6a51ad3c152659b415534fd830b830eb4430
clarified use of options;

diff -r 09df6a51ad3c -r 22a17cec2efe src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sat Mar 26 12:22:15 2016 +0100
+++ b/src/Pure/System/isabelle_process.ML	Sat Mar 26 12:35:11 2016 +0100
@@ -210,7 +210,8 @@
 (* init options *)
 
 fun init_options () =
- (Future.ML_statistics := Options.default_bool "ML_statistics";
+ (ML_Pretty.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");
   Goal.parallel_proofs := Options.default_int "parallel_proofs");
diff -r 09df6a51ad3c -r 22a17cec2efe src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Sat Mar 26 12:22:15 2016 +0100
+++ b/src/Pure/System/options.ML	Sat Mar 26 12:35:11 2016 +0100
@@ -216,6 +216,6 @@
       end);
 
 val _ = load_default ();
+val _ = ML_Pretty.print_depth (default_int "ML_print_depth");
 
 end;
-
diff -r 09df6a51ad3c -r 22a17cec2efe src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Sat Mar 26 12:22:15 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Sat Mar 26 12:35:11 2016 +0100
@@ -66,17 +66,15 @@
     val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
 
-    val print_depth = ML_Syntax.print_int(options.int("ML_print_depth"))
     val eval_process =
       if (heaps.isEmpty)
-        List("PolyML.print_depth " + print_depth)
+        List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
       else
         channel match {
           case None =>
-            List("(ML_Pretty.print_depth " + print_depth + "; Isabelle_Process.init_options ())")
+            List("Isabelle_Process.init_options ()")
           case Some(ch) =>
-            List("(ML_Pretty.print_depth " + print_depth + "; Isabelle_Process.init_protocol " +
-              ML_Syntax.print_string0(ch.server_name) + ")")
+            List("Isabelle_Process.init_protocol " + ML_Syntax.print_string0(ch.server_name))
         }
 
     // ISABELLE_TMP