# HG changeset patch
# User wenzelm
# Date 1384601350 -3600
# Node ID 9714b5474f391b71022d572f4cd659bc2c2c2750
# Parent  c39972ddd6723d3e09e47ec17587efdb49db5419
more distinctive Isabelle_Process.Output vs. Isabelle_Process.Protocol_Output;

diff -r c39972ddd672 -r 9714b5474f39 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri Nov 15 19:31:10 2013 +0100
+++ b/src/Pure/System/isabelle_process.scala	Sat Nov 16 12:29:10 2013 +0100
@@ -43,13 +43,12 @@
     def is_system = kind == Markup.SYSTEM
     def is_status = kind == Markup.STATUS
     def is_report = kind == Markup.REPORT
-    def is_protocol = kind == Markup.PROTOCOL
     def is_syslog = is_init || is_exit || is_system || is_stderr
 
     override def toString: String =
     {
       val res =
-        if (is_status || is_report || is_protocol) message.body.map(_.toString).mkString
+        if (is_status || is_report) message.body.map(_.toString).mkString
         else Pretty.string_of(message.body)
       if (properties.isEmpty)
         kind.toString + " [[" + res + "]]"
diff -r c39972ddd672 -r 9714b5474f39 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Nov 15 19:31:10 2013 +0100
+++ b/src/Pure/System/session.scala	Sat Nov 16 12:29:10 2013 +0100
@@ -281,17 +281,16 @@
         msg match {
           case _: Isabelle_Process.Input =>
             buffer += msg
+          case output: Isabelle_Process.Protocol_Output if output.properties == Markup.Flush =>
+            flush()
           case output: Isabelle_Process.Output =>
-            if (output.is_protocol && output.properties == Markup.Flush) flush()
-            else {
-              buffer += msg
-              if (output.is_syslog)
-                syslog >> (queue =>
-                  {
-                    val queue1 = queue.enqueue(output.message)
-                    if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
-                  })
-            }
+            buffer += msg
+            if (output.is_syslog)
+              syslog >> (queue =>
+                {
+                  val queue1 = queue.enqueue(output.message)
+                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
+                })
         }
       }