src/Pure/Tools/server.scala
changeset 69451 387894c2fb2c
parent 69448 51e696887b81
child 69458 5655af3ea5bd
--- a/src/Pure/Tools/server.scala	Tue Dec 11 23:59:41 2018 +0100
+++ b/src/Pure/Tools/server.scala	Wed Dec 12 00:01:11 2018 +0100
@@ -181,7 +181,8 @@
         interrupt = interrupt)
 
     def read_message(): Option[String] =
-      Byte_Message.read_line_message(in).map(_.text)
+      try { Byte_Message.read_line_message(in).map(_.text) }
+      catch { case _: IOException => None }
 
     def write_message(msg: String): Unit =
       out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) }