# HG changeset patch
# User wenzelm
# Date 1284919911 -7200
# Node ID f1296795a8dca1b836b2934be40150eb87a89c90
# Parent  72e949a0425bbdafdde1d6b30678f6c79f1b0644
message_actor: more robust treatment of EOF;

diff -r 72e949a0425b -r f1296795a8dc src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sun Sep 19 17:12:34 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sun Sep 19 20:11:51 2010 +0200
@@ -241,9 +241,11 @@
 
   /* message output */
 
-  private class Protocol_Error(msg: String) extends Exception(msg)
+  private def message_actor(name: String, fifo: String): Actor =
+  {
+    class EOF extends Exception
+    class Protocol_Error(msg: String) extends Exception(msg)
 
-  private def message_actor(name: String, fifo: String): Actor =
     Simple_Thread.actor(name) {
       val stream = system.fifo_input_stream(fifo)  // FIXME potentially blocking forever
       val default_buffer = new Array[Byte](65536)
@@ -255,6 +257,7 @@
         // chunk size
         var n = 0
         c = stream.read
+        if (c == -1) throw new EOF
         while (48 <= c && c <= 57) {
           n = 10 * n + (c - 48)
           c = stream.read
@@ -293,6 +296,7 @@
         catch {
           case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
           case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
+          case _: EOF =>
         }
       } while (c != -1)
       stream.close
@@ -300,6 +304,7 @@
 
       system_result(name + " terminated")
     }
+  }