src/Pure/ML/ml_console.scala

--- a/src/Pure/ML/ml_console.scala	Sat Mar 10 12:51:04 2018 +0100
+++ b/src/Pure/ML/ml_console.scala	Sat Mar 10 13:03:01 2018 +0100
@@ -74,7 +74,7 @@
             if (raw_ml_system) None
             else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
 
-      val tty_loop = new TTY_Loop(process.stdin, process.stdout, process.interrupt _)
+      val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _))
       val process_result = Future.thread[Int]("process_result") {
         val rc = process.join
         tty_loop.cancel  // FIXME does not quite work, cannot interrupt blocking read on System.in