Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified interactive mode, which is relevant for ML prompts;
authorwenzelm
Wed, 09 Mar 2016 20:44:02 +0100
changeset 62577 7e2aa1d67dd8
parent 62576 26179aa33fe7
child 62578 739a84403864
clarified interactive mode, which is relevant for ML prompts;
src/Pure/System/ml_process.scala file | annotate | diff | comparison | revisions
src/Pure/Tools/ml_console.scala file | annotate | diff | comparison | revisions 
--- 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"
--- 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 {
isabelle