more comments;

--- a/src/Pure/ML/ml_console.scala	Fri Mar 09 17:03:10 2018 +0100
+++ b/src/Pure/ML/ml_console.scala	Sat Mar 10 11:08:20 2018 +0100
@@ -77,7 +77,7 @@
       val tty_loop = new TTY_Loop(process.stdin, process.stdout, process.interrupt _)
       val process_result = Future.thread[Int]("process_result") {
         val rc = process.join
-        tty_loop.cancel
+        tty_loop.cancel  // FIXME does not quite work, cannot interrupt blocking read on System.in
         rc
       }
       tty_loop.join