# HG changeset patch
# User wenzelm
# Date 1330724082 -3600
# Node ID d52a4f2eeb7487c711accca93c2b01c211b572ec
# Parent  b0a797158e340c01dee5ee7691e73ef9416dc271
terminate after first exception -- avoid syslog flooding;

diff -r b0a797158e34 -r d52a4f2eeb74 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri Mar 02 21:22:42 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Mar 02 22:34:42 2012 +0100
@@ -234,7 +234,9 @@
           }
           //}}}
         }
-        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
+        catch {
+          case e: IOException => finished = true; system_result(name + ": " + e.getMessage)
+        }
       }
       system_result(name + " terminated")
     }
@@ -273,7 +275,9 @@
           }
           //}}}
         }
-        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
+        catch {
+          case e: IOException => finished; system_result(name + ": " + e.getMessage)
+        }
       }
       system_result(name + " terminated")
     }
@@ -304,7 +308,9 @@
           }
           //}}}
         }
-        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
+        catch {
+          case e: IOException => finished; system_result(name + ": " + e.getMessage)
+        }
       }
       system_result(name + " terminated")
     }
@@ -371,8 +377,8 @@
           }
         }
         catch {
-          case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
-          case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
+          case e: IOException => c = -1; system_result("Cannot read message:\n" + e.getMessage)
+          case e: Protocol_Error => c = -1; system_result("Malformed message:\n" + e.getMessage)
           case _: EOF =>
         }
       } while (c != -1)