terminate after first exception -- avoid syslog flooding;
authorwenzelm
Fri, 02 Mar 2012 22:34:42 +0100
changeset 46762 d52a4f2eeb74
parent 46761 b0a797158e34
child 46766 4269ae06afc5
terminate after first exception -- avoid syslog flooding;
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)