# HG changeset patch
# User wenzelm
# Date 1457552189 -3600
# Node ID 26179aa33fe70d86e7573a5e0be3f439e44c4f25
# Parent  590df5f4e531fb3e938f8acfa2bba62edbeb1931
more careful print_depth on startup;

diff -r 590df5f4e531 -r 26179aa33fe7 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Wed Mar 09 20:11:25 2016 +0100
+++ b/src/Doc/System/Basics.thy	Wed Mar 09 20:36:29 2016 +0100
@@ -335,9 +335,6 @@
   theory value from the theory loader within ML (observe the delicate quoting
   rules for the Bash shell vs.\ ML):
   @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
-
-  Note that the output text will be interspersed with additional junk messages
-  by the ML runtime environment.
 \<close>
 
 
diff -r 590df5f4e531 -r 26179aa33fe7 src/Pure/System/ml_process.scala
--- a/src/Pure/System/ml_process.scala	Wed Mar 09 20:11:25 2016 +0100
+++ b/src/Pure/System/ml_process.scala	Wed Mar 09 20:36:29 2016 +0100
@@ -44,8 +44,8 @@
 
     val eval_heaps =
       load_heaps.map(load_heap =>
-        "PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) +
-        " handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
+        "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) +
+        "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
         ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") +
         "); OS.Process.exit OS.Process.failure)")
 
@@ -59,8 +59,7 @@
           else
             "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
           "PolyML.Compiler.prompt1 := \"ML> \"",
-          "PolyML.Compiler.prompt2 := \"ML# \"",
-          "PolyML.print_depth 10")
+          "PolyML.Compiler.prompt2 := \"ML# \"")
       }
       else Nil
 
@@ -77,13 +76,15 @@
     val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
 
     val eval_process =
-      if (load_heaps.isEmpty) Nil
+      if (load_heaps.isEmpty)
+        List("PolyML.print_depth 10")
       else
         channel match {
           case None =>
-            List("Isabelle_Process.init_options ()")
+            List("(default_print_depth 10; Isabelle_Process.init_options ())")
           case Some(ch) =>
-            List("Isabelle_Process.init_protocol " + ML_Syntax.print_string_raw(ch.server_name))
+            List("(default_print_depth 10; Isabelle_Process.init_protocol " +
+              ML_Syntax.print_string_raw(ch.server_name) + ")")
         }
 
     // bash