# HG changeset patch
# User wenzelm
# Date 1457552642 -3600
# Node ID 7e2aa1d67dd8e7324f19ba6fbc3fcc7e166d9d20
# Parent  26179aa33fe70d86e7573a5e0be3f439e44c4f25
clarified interactive mode, which is relevant for ML prompts;

diff -r 26179aa33fe7 -r 7e2aa1d67dd8 src/Pure/System/ml_process.scala
--- a/src/Pure/System/ml_process.scala	Wed Mar 09 20:36:29 2016 +0100
+++ b/src/Pure/System/ml_process.scala	Wed Mar 09 20:44:02 2016 +0100
@@ -103,7 +103,7 @@
         chmod $(umask -S) "$ISABELLE_TMP"
 
         librarypath "$ML_HOME"
-        "$ML_HOME/poly" -q -i """ + File.bash_args(bash_args) + """
+        "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
         RC="$?"
 
         rm -f "$ISABELLE_PROCESS_OPTIONS"
diff -r 26179aa33fe7 -r 7e2aa1d67dd8 src/Pure/Tools/ml_console.scala
--- a/src/Pure/Tools/ml_console.scala	Wed Mar 09 20:36:29 2016 +0100
+++ b/src/Pure/Tools/ml_console.scala	Wed Mar 09 20:44:02 2016 +0100
@@ -68,7 +68,7 @@
 
       // process loop
       val process =
-        ML_Process(options, heap = logic,
+        ML_Process(options, heap = logic, args = List("-i"),
           modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"))
       val process_output = Future.thread[Unit]("process_output") {
         try {