clarified RAW_ML_SYSTEM;
authorwenzelm
Mon, 07 Mar 2016 18:47:55 +0100
changeset 62547 b33dea503665
parent 62546 973b12bccbc5
child 62548 f8ebb715e06d
clarified RAW_ML_SYSTEM;
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