# HG changeset patch
# User wenzelm
# Date 1586200058 -7200
# Node ID 928fd852f3e2d797bafd75c1d1cbdbcd4c8f0c16
# Parent  c6b7f4da67b3f27601dfd69cfa62c6328a51261f
more robust interrupt handling;

diff -r c6b7f4da67b3 -r 928fd852f3e2 src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Mon Apr 06 21:04:33 2020 +0200
+++ b/src/Pure/ML/ml_console.scala	Mon Apr 06 21:07:38 2020 +0200
@@ -74,16 +74,11 @@
             else Some(Sessions.base_info(
               options, logic, dirs = dirs, include_sessions = include_sessions).check_base))
 
-      val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _))
-      val process_result = Future.thread[Int]("process_result") {
+      POSIX_Interrupt.handler { process.interrupt } {
+        new TTY_Loop(process.stdin, process.stdout).join
         val rc = process.join
-        tty_loop.cancel  // FIXME does not quite work, cannot interrupt blocking read on System.in
-        rc
+        if (rc != 0) sys.exit(rc)
       }
-      tty_loop.join
-
-      val rc = process_result.join
-      if (rc != 0) sys.exit(rc)
     }
   }
 }
diff -r c6b7f4da67b3 -r 928fd852f3e2 src/Pure/System/tty_loop.scala
--- a/src/Pure/System/tty_loop.scala	Mon Apr 06 21:04:33 2020 +0200
+++ b/src/Pure/System/tty_loop.scala	Mon Apr 06 21:07:38 2020 +0200
@@ -10,13 +10,14 @@
 import java.io.{IOException, Writer, Reader, InputStreamReader, BufferedReader}
 
 
-class TTY_Loop(writer: Writer, reader: Reader,
-  writer_lock: AnyRef = new Object,
-  interrupt: Option[() => Unit] = None)
+class TTY_Loop(
+  writer: Writer,
+  reader: Reader,
+  writer_lock: AnyRef = new Object)
 {
-  private val console_output = Future.thread[Unit]("console_output") {
+  private val console_output = Future.thread[Unit]("console_output", uninterruptible = true) {
     try {
-      var result = new StringBuilder(100)
+      val result = new StringBuilder(100)
       var finished = false
       while (!finished) {
         var c = -1
@@ -40,32 +41,25 @@
     catch { case e: IOException => case Exn.Interrupt() => }
   }
 
-  private val console_input = Future.thread[Unit]("console_input") {
+  private val console_input = Future.thread[Unit]("console_input", uninterruptible = true) {
     val console_reader = new BufferedReader(new InputStreamReader(System.in))
-    def body
-    {
-      try {
-        var finished = false
-        while (!finished) {
-          console_reader.readLine() match {
-            case null =>
-              writer.close()
-              finished = true
-            case line =>
-              writer_lock.synchronized {
-                writer.write(line)
-                writer.write("\n")
-                writer.flush()
-              }
-          }
+    try {
+      var finished = false
+      while (!finished) {
+        console_reader.readLine() match {
+          case null =>
+            writer.close()
+            finished = true
+          case line =>
+            writer_lock.synchronized {
+              writer.write(line)
+              writer.write("\n")
+              writer.flush()
+            }
         }
       }
-      catch { case e: IOException => case Exn.Interrupt() => }
     }
-    interrupt match {
-      case None => body
-      case Some(int) => POSIX_Interrupt.handler { int() } { body }
-    }
+    catch { case e: IOException => case Exn.Interrupt() => }
   }
 
   def join { console_output.join; console_input.join }
diff -r c6b7f4da67b3 -r 928fd852f3e2 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Mon Apr 06 21:04:33 2020 +0200
+++ b/src/Pure/Tools/server.scala	Mon Apr 06 21:07:38 2020 +0200
@@ -173,12 +173,11 @@
     private val out = new BufferedOutputStream(socket.getOutputStream)
     private val out_lock: AnyRef = new Object
 
-    def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop =
+    def tty_loop(): TTY_Loop =
       new TTY_Loop(
         new OutputStreamWriter(out),
         new InputStreamReader(in),
-        writer_lock = out_lock,
-        interrupt = interrupt)
+        writer_lock = out_lock)
 
     def read_password(password: String): Boolean =
       try { Byte_Message.read_line(in).map(_.text) == Some(password) }