# HG changeset patch
# User wenzelm
# Date 1457372875 -3600
# Node ID b33dea50366597401ff2363b697f897ac52038c5
# Parent  973b12bccbc5dd8e0d889777293d8754d9f1d0c7
clarified RAW_ML_SYSTEM;

diff -r 973b12bccbc5 -r b33dea503665 src/Pure/System/ml_process.scala
--- a/src/Pure/System/ml_process.scala	Mon Mar 07 18:31:40 2016 +0100
+++ b/src/Pure/System/ml_process.scala	Mon Mar 07 18:47:55 2016 +0100
@@ -50,9 +50,8 @@
             "fun exit 0 = OS.Process.exit OS.Process.success" +
             " | exit 1 = OS.Process.exit OS.Process.failure" +
             " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
-          else
-            "fun exit rc = Posix.Process.exit (Word8.fromInt rc)"
-        )
+          else "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
+          "PolyML.print_depth 10")
       }
       else Nil
 
@@ -67,7 +66,7 @@
     val isabelle_process_options = Isabelle_System.tmp_file("options")
     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
     val env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
-    val eval_options = List("Options.load_default ()")
+    val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()")
 
     val eval_process =
       if (process_socket == "") Nil