# HG changeset patch
# User wenzelm
# Date 1243978721 -7200
# Node ID 6c1b0e7186fe9cf669566e94407f7ae503a1f862
# Parent  4f2d122c0a67b5365a5f9c96d445646e2261e055# Parent  d461e5506d02ada8c6c9cb194fd623205a934728
merged

diff -r 4f2d122c0a67 -r 6c1b0e7186fe src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 02 22:55:20 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 02 23:38:41 2009 +0200
@@ -113,17 +113,16 @@
           else (false, null)
       }
 
-    if (result.kind == IsabelleProcess.Kind.STDOUT || result.kind == IsabelleProcess.Kind.STDIN)
+    if (result.kind == IsabelleProcess.Kind.STDOUT ||
+        result.kind == IsabelleProcess.Kind.STDIN)
       output_info.event(result.toString)
-    else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) {  // FIXME !?
-      initialized = true
-      Swing.now { this ! ProverEvents.Activate }
-    }
     else {
       result.kind match {
 
-        case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
-          | IsabelleProcess.Kind.WARNING | IsabelleProcess.Kind.ERROR =>
+        case IsabelleProcess.Kind.WRITELN
+        | IsabelleProcess.Kind.PRIORITY
+        | IsabelleProcess.Kind.WARNING
+        | IsabelleProcess.Kind.ERROR =>
           if (command != null) {
             if (result.kind == IsabelleProcess.Kind.ERROR)
               command.status = Command.Status.FAILED
@@ -147,6 +146,12 @@
                   case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
                     keyword_decls += name
 
+                  // process ready (after initialization)
+                  case XML.Elem(Markup.READY, _, _)
+                  if !initialized =>
+                    initialized = true
+                    Swing.now { this ! ProverEvents.Activate }
+
                   // document edits
                   case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
                   if document_versions.exists(_.id == doc_id) =>