more distinctive Isabelle_Process.Output vs. Isabelle_Process.Protocol_Output;
--- 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 + "]]"
--- 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
+ })
}
}