# HG changeset patch
# User wenzelm
# Date 1631199220 -7200
# Node ID 0a4cdf0036a08933ed4fa81139b700ec9e5cf267
# Parent  0f3ca0cd8071f66b96dac8150ac63c489bb09ce2
more robust: client could have terminated already;

diff -r 0f3ca0cd8071 -r 0a4cdf0036a0 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(