more general TTY loop;

--- 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
     }
   }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/tty_loop.scala	Fri Mar 09 17:03:10 2018 +0100
@@ -0,0 +1,68 @@
+/*  Title:      Pure/System/tty_loop.scala
+    Author:     Makarius
+
+Line-oriented TTY loop.
+*/
+
+package isabelle
+
+
+import java.io.{IOException, BufferedReader, BufferedWriter, InputStreamReader}
+
+
+class TTY_Loop(
+  process_writer: BufferedWriter,
+  process_reader: BufferedReader,
+  process_interrupt: () => Unit = () => ())
+{
+  private val console_output = Future.thread[Unit]("console_output") {
+    try {
+      var result = new StringBuilder(100)
+      var finished = false
+      while (!finished) {
+        var c = -1
+        var done = false
+        while (!done && (result.length == 0 || process_reader.ready)) {
+          c = process_reader.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_reader.close()
+          finished = true
+        }
+      }
+    }
+    catch { case e: IOException => case Exn.Interrupt() => }
+  }
+
+  private val console_input = Future.thread[Unit]("console_input") {
+    val console_reader = new BufferedReader(new InputStreamReader(System.in))
+    POSIX_Interrupt.handler { process_interrupt() } {
+      try {
+        var finished = false
+        while (!finished) {
+          console_reader.readLine() match {
+            case null =>
+              process_writer.close()
+              finished = true
+            case line =>
+              process_writer.write(line)
+              process_writer.write("\n")
+              process_writer.flush()
+          }
+        }
+      }
+      catch { case e: IOException => case Exn.Interrupt() => }
+    }
+  }
+
+  def join { console_output.join; console_input.join }
+
+  def cancel { console_input.cancel }
+}

--- a/src/Pure/build-jars	Fri Mar 09 15:43:54 2018 +0100
+++ b/src/Pure/build-jars	Fri Mar 09 17:03:10 2018 +0100
@@ -127,6 +127,7 @@
   System/process_result.scala
   System/progress.scala
   System/system_channel.scala
+  System/tty_loop.scala
   Thy/bibtex.scala
   Thy/html.scala
   Thy/latex.scala