# HG changeset patch
# User wenzelm
# Date 1285245569 -7200
# Node ID fb0c851e4f9d9c64c6e25a2e427cc20bcd64d126
# Parent  57496c868dcccee431ac31bfb14fc008d6d3de4a
tuned prover message categorization;

diff -r 57496c868dcc -r fb0c851e4f9d src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Thu Sep 23 14:26:55 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Thu Sep 23 14:39:29 2010 +0200
@@ -72,7 +72,14 @@
 
   /* specific messages */
 
-  def is_tracing(msg: XML.Tree): Boolean =
+  def is_ready(msg: XML.Tree): Boolean =
+    msg match {
+      case XML.Elem(Markup(Markup.STATUS, _),
+        List(XML.Elem(Markup(Markup.READY, _), _))) => true
+      case _ => false
+    }
+
+ def is_tracing(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.TRACING, _), _) => true
       case _ => false
diff -r 57496c868dcc -r fb0c851e4f9d src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu Sep 23 14:26:55 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Sep 23 14:39:29 2010 +0200
@@ -44,11 +44,8 @@
     def is_system = kind == Markup.SYSTEM
     def is_status = kind == Markup.STATUS
     def is_report = kind == Markup.REPORT
-    def is_ready = is_status && {
-      body match {
-        case List(XML.Elem(Markup(Markup.READY, _), _)) => true
-        case _ => false
-      }}
+    def is_ready = Isar_Document.is_ready(message)
+    def is_syslog = is_init || is_exit || is_system || is_ready
 
     override def toString: String =
     {
diff -r 57496c868dcc -r fb0c851e4f9d src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Sep 23 14:26:55 2010 +0200
+++ b/src/Pure/System/session.scala	Thu Sep 23 14:39:29 2010 +0200
@@ -187,7 +187,9 @@
           }
           catch { case _: Document.State.Fail => bad_result(result) }
         case _ =>
-          if (result.is_status) {
+          if (result.is_exit) prover = null  // FIXME ??
+          else if (result.is_syslog || result.is_stdout) { }
+          else if (result.is_status) {
             result.body match {
               case List(Isar_Document.Assign(id, edits)) =>
                 try {
@@ -198,12 +200,10 @@
                 catch { case _: Document.State.Fail => bad_result(result) }
               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
               case List(Keyword.Keyword_Decl(name)) => syntax += name
-              case _ => if (!result.is_ready) bad_result(result)
+              case _ => bad_result(result)
             }
           }
-          else if (result.is_exit) prover = null  // FIXME ??
-          else if (!(result.is_init || result.is_exit || result.is_system || result.is_stdout))
-            bad_result(result)
+          else bad_result(result)
         }
     }
     //}}}
diff -r 57496c868dcc -r fb0c851e4f9d src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 14:26:55 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 14:39:29 2010 +0200
@@ -53,8 +53,10 @@
     loop {
       react {
         case result: Isabelle_Process.Result =>
-          if (result.is_init || result.is_exit || result.is_system || result.is_ready)
-            Swing_Thread.now { syslog.append(XML.content(result.message).mkString + "\n") }
+          if (result.is_syslog)
+            Swing_Thread.now {
+              syslog.append(XML.content(result.message).mkString + "\n")
+            }
 
         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
       }