diff -r 8f5f5fbe291b -r 32d76f08023f src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Fri Mar 09 15:43:54 2018 +0100
+++ b/src/Pure/ML/ml_console.scala	Fri Mar 09 17:03:10 2018 +0100
@@ -7,9 +7,6 @@
 package isabelle
 
 
-import java.io.{IOException, BufferedReader, InputStreamReader}
-
-
 object ML_Console
 {
   /* command line entry point */
@@ -76,59 +73,14 @@
           session_base =
             if (raw_ml_system) None
             else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
-      val process_output = Future.thread[Unit]("process_output") {
-        try {
-          var result = new StringBuilder(100)
-          var finished = false
-          while (!finished) {
-            var c = -1
-            var done = false
-            while (!done && (result.length == 0 || process.stdout.ready)) {
-              c = process.stdout.read
-              if (c >= 0) result.append(c.asInstanceOf[Char])
-              else done = true
-            }
-            if (result.length > 0) {
-              System.out.print(result.toString)
-              System.out.flush()
-              result.length = 0
-            }
-            else {
-              process.stdout.close()
-              finished = true
-            }
-          }
-        }
-        catch { case e: IOException => case Exn.Interrupt() => }
-      }
-      val process_input = Future.thread[Unit]("process_input") {
-        val reader = new BufferedReader(new InputStreamReader(System.in))
-        POSIX_Interrupt.handler { process.interrupt } {
-          try {
-            var finished = false
-            while (!finished) {
-              reader.readLine() match {
-                case null =>
-                  process.stdin.close()
-                  finished = true
-                case line =>
-                  process.stdin.write(line)
-                  process.stdin.write("\n")
-                  process.stdin.flush()
-              }
-            }
-          }
-          catch { case e: IOException => case Exn.Interrupt() => }
-        }
-      }
+
+      val tty_loop = new TTY_Loop(process.stdin, process.stdout, process.interrupt _)
       val process_result = Future.thread[Int]("process_result") {
         val rc = process.join
-        process_input.cancel
+        tty_loop.cancel
         rc
       }
-
-      process_output.join
-      process_input.join
+      tty_loop.join
       process_result.join
     }
   }