# HG changeset patch
# User wenzelm
# Date 1520683381 -3600
# Node ID 9cb7f5f0bf416784e0df3ef227fc74db2598e65d
# Parent  331619e6c8b0ce08dc145f5988a1327824a001c0
clarified interrupt handling;

diff -r 331619e6c8b0 -r 9cb7f5f0bf41 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
diff -r 331619e6c8b0 -r 9cb7f5f0bf41 src/Pure/System/tty_loop.scala
--- a/src/Pure/System/tty_loop.scala	Sat Mar 10 12:51:04 2018 +0100
+++ b/src/Pure/System/tty_loop.scala	Sat Mar 10 13:03:01 2018 +0100
@@ -13,7 +13,7 @@
 class TTY_Loop(
   process_writer: BufferedWriter,
   process_reader: BufferedReader,
-  process_interrupt: () => Unit = () => ())
+  process_interrupt: Option[() => Unit] = None)
 {
   private val console_output = Future.thread[Unit]("console_output") {
     try {
@@ -43,7 +43,8 @@
 
   private val console_input = Future.thread[Unit]("console_input") {
     val console_reader = new BufferedReader(new InputStreamReader(System.in))
-    POSIX_Interrupt.handler { process_interrupt() } {
+    def body
+    {
       try {
         var finished = false
         while (!finished) {
@@ -60,6 +61,11 @@
       }
       catch { case e: IOException => case Exn.Interrupt() => }
     }
+    process_interrupt match {
+      case None => body
+      case Some(interrupt) =>
+        POSIX_Interrupt.handler { interrupt() } { body }
+    }
   }
 
   def join { console_output.join; console_input.join }