avoid hardwired values;

--- a/etc/options	Sat Mar 26 12:17:02 2016 +0100
+++ b/etc/options	Sat Mar 26 12:22:15 2016 +0100
@@ -104,6 +104,9 @@
 
 section "ML System"
 
+option ML_print_depth : int = 20
+  -- "ML print depth for toplevel pretty-printing"
+
 public option ML_exception_trace : bool = false
   -- "ML exception trace for toplevel command execution"
 

--- a/src/HOL/Metis.thy	Sat Mar 26 12:17:02 2016 +0100
+++ b/src/HOL/Metis.thy	Sat Mar 26 12:22:15 2016 +0100
@@ -10,9 +10,7 @@
 imports ATP
 begin
 
-declare [[ML_print_depth = 0]]
 ML_file "~~/src/Tools/Metis/metis.ML"
-declare [[ML_print_depth = 20]]
 
 
 subsection \<open>Literal selection and lambda-lifting helpers\<close>

--- a/src/Pure/ML/ml_pretty.ML	Sat Mar 26 12:17:02 2016 +0100
+++ b/src/Pure/ML/ml_pretty.ML	Sat Mar 26 12:22:15 2016 +0100
@@ -96,7 +96,6 @@
 in
   fun get_print_depth () = ! depth;
   fun print_depth n = (depth := n; PolyML.print_depth n);
-  val _ = print_depth 20;
 end;
 
 

--- a/src/Pure/Tools/ml_process.scala	Sat Mar 26 12:17:02 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Sat Mar 26 12:22:15 2016 +0100
@@ -66,15 +66,16 @@
     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 20")
+        List("PolyML.print_depth " + print_depth)
       else
         channel match {
           case None =>
-            List("(ML_Pretty.print_depth 20; Isabelle_Process.init_options ())")
+            List("(ML_Pretty.print_depth " + print_depth + "; Isabelle_Process.init_options ())")
           case Some(ch) =>
-            List("(ML_Pretty.print_depth 20; Isabelle_Process.init_protocol " +
+            List("(ML_Pretty.print_depth " + print_depth + "; Isabelle_Process.init_protocol " +
               ML_Syntax.print_string0(ch.server_name) + ")")
         }