# HG changeset patch
# User wenzelm
# Date 1243978656 -7200
# Node ID d461e5506d02ada8c6c9cb194fd623205a934728
# Parent  e8ac8794971fb0cc6a182dc8bced266036132fbf
handle_result: activate via explicit status "ready" (cf. http://isabelle.in.tum.de/repos/isabelle/rev/ce169bd37fc0);
tuned;

diff -r e8ac8794971f -r d461e5506d02 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 02 22:31:58 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 02 23:37:36 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) =>