# HG changeset patch
# User immler@in.tum.de
# Date 1251363069 -7200
# Node ID 85222d00f5ec882519a8f1f039707b9e7a8083a9
# Parent  9e725d34df7bb78a9a7166fe7b8815b2f610e85b
catching NPE on val

diff -r 9e725d34df7b -r 85222d00f5ec src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -103,7 +103,14 @@
           else None
       }
     output_info.event(result)
-    val message = process.parse_message(result)
+    val message =
+      try{process.parse_message(result)}
+        /* handle_results can be called before val process is initialized */
+      catch {
+        case e: NullPointerException =>
+          System.err.println("NPE; did not handle_result: " + result)
+      }
+
     if (state.isDefined) state.get ! message
     else result.kind match {