more robust: client could have terminated already;
authorwenzelm
Thu, 09 Sep 2021 16:53:40 +0200
changeset 74273 0a4cdf0036a0
parent 74272 0f3ca0cd8071
child 74274 36f2c4a5c21b
more robust: client could have terminated already;
src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Thu Sep 09 16:00:34 2021 +0200
+++ b/src/Pure/System/bash.scala	Thu Sep 09 16:53:40 2021 +0200
@@ -8,8 +8,9 @@
 package isabelle
 
 
-import java.util.{LinkedList, List => JList, Map => JMap}
-import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, File => JFile}
+import java.util.{List => JList, Map => JMap}
+import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
+  File => JFile, IOException}
 import scala.annotation.tailrec
 import scala.jdk.OptionConverters._
 
@@ -282,7 +283,8 @@
     override def handle(connection: isabelle.Server.Connection): Unit =
     {
       def reply(chunks: List[String]): Unit =
-        connection.write_byte_message(chunks.map(Bytes.apply))
+        try { connection.write_byte_message(chunks.map(Bytes.apply)) }
+        catch { case _: IOException => }
 
       def reply_failure(exn: Throwable): Unit =
         reply(