message_actor: more robust treatment of EOF;
authorwenzelm
Sun Sep 19 20:11:51 2010 +0200 (2010-09-19 ago)
changeset 39526f1296795a8dc
parent 39525 72e949a0425b
child 39527 f03a9c57760a
message_actor: more robust treatment of EOF;
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/System/isabelle_process.scala	Sun Sep 19 17:12:34 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Sep 19 20:11:51 2010 +0200
     1.3 @@ -241,9 +241,11 @@
     1.4  
     1.5    /* message output */
     1.6  
     1.7 -  private class Protocol_Error(msg: String) extends Exception(msg)
     1.8 +  private def message_actor(name: String, fifo: String): Actor =
     1.9 +  {
    1.10 +    class EOF extends Exception
    1.11 +    class Protocol_Error(msg: String) extends Exception(msg)
    1.12  
    1.13 -  private def message_actor(name: String, fifo: String): Actor =
    1.14      Simple_Thread.actor(name) {
    1.15        val stream = system.fifo_input_stream(fifo)  // FIXME potentially blocking forever
    1.16        val default_buffer = new Array[Byte](65536)
    1.17 @@ -255,6 +257,7 @@
    1.18          // chunk size
    1.19          var n = 0
    1.20          c = stream.read
    1.21 +        if (c == -1) throw new EOF
    1.22          while (48 <= c && c <= 57) {
    1.23            n = 10 * n + (c - 48)
    1.24            c = stream.read
    1.25 @@ -293,6 +296,7 @@
    1.26          catch {
    1.27            case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
    1.28            case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
    1.29 +          case _: EOF =>
    1.30          }
    1.31        } while (c != -1)
    1.32        stream.close
    1.33 @@ -300,6 +304,7 @@
    1.34  
    1.35        system_result(name + " terminated")
    1.36      }
    1.37 +  }
    1.38  
    1.39  
    1.40