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))) }