# HG changeset patch
# User wenzelm
# Date 1457458709 -3600
# Node ID 498f6ff1680416a6d2680698a22b6ac9da0604a6
# Parent  83e815849a917ffd75f9bec2a858e19bf8f4dd18
clarified initial ML;

diff -r 83e815849a91 -r 498f6ff16804 src/Pure/System/ml_process.scala
--- a/src/Pure/System/ml_process.scala	Tue Mar 08 18:15:16 2016 +0100
+++ b/src/Pure/System/ml_process.scala	Tue Mar 08 18:38:29 2016 +0100
@@ -44,14 +44,17 @@
         ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") +
         "); OS.Process.exit OS.Process.failure)")
 
-    val eval_exit =
+    val eval_initial =
       if (load_heaps.isEmpty) {
         List(
           if (Platform.is_windows)
             "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.Compiler.prompt1 := \"ML> \"",
+          "PolyML.Compiler.prompt2 := \"ML# \"",
           "PolyML.print_depth 10")
       }
       else Nil
@@ -75,7 +78,7 @@
     // bash
     val bash_args =
       Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
-      (eval_heaps ::: eval_exit ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
+      (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
         map(eval => List("--eval", eval)).flatten ::: args
 
     Bash.process(env = env, redirect = redirect, script =