# HG changeset patch
# User wenzelm
# Date 1398462145 -7200
# Node ID f7700146678d95986d5bd947a4234d212bbd108b
# Parent  da3fefcb43c3c3199c418d59ce3cee7afc5a3948
manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);

diff -r da3fefcb43c3 -r f7700146678d src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Apr 25 23:29:54 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Apr 25 23:42:25 2014 +0200
@@ -172,7 +172,6 @@
   val padding_command: Properties.entry
   val dialogN: string val dialog: serial -> string -> T
   val functionN: string
-  val flush: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
   val protocol_handler: string -> Properties.T
@@ -557,8 +556,6 @@
 
 val functionN = "function"
 
-val flush = [(functionN, "flush")];
-
 val assign_update = [(functionN, "assign_update")];
 val removed_versions = [(functionN, "removed_versions")];
 
diff -r da3fefcb43c3 -r f7700146678d src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Apr 25 23:29:54 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Apr 25 23:42:25 2014 +0200
@@ -365,8 +365,6 @@
   val FUNCTION = "function"
   val Function = new Properties.String(FUNCTION)
 
-  val Flush: Properties.T = List((FUNCTION, "flush"))
-
   val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
   val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
 
diff -r da3fefcb43c3 -r f7700146678d src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Apr 25 23:29:54 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Apr 25 23:42:25 2014 +0200
@@ -261,7 +261,6 @@
   private case object Stop
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command(name: String, args: List[String])
-  private case class Messages(msgs: List[Prover.Message])
   private case class Update_Options(options: Options)
 
 
@@ -300,44 +299,6 @@
   }
 
 
-  /* buffered prover messages */
-
-  private object receiver
-  {
-    private var buffer = new mutable.ListBuffer[Prover.Message]
-
-    private def flush(): Unit = synchronized {
-      if (!buffer.isEmpty) {
-        val msgs = buffer.toList
-        manager.send(Messages(msgs))
-        buffer = new mutable.ListBuffer[Prover.Message]
-      }
-    }
-
-    def invoke(msg: Prover.Message): Unit = synchronized {
-      msg match {
-        case _: Prover.Input =>
-          buffer += msg
-        case output: Prover.Protocol_Output if output.properties == Markup.Flush =>
-          flush()
-        case output: Prover.Output =>
-          buffer += msg
-          if (output.is_syslog)
-            syslog.change(queue =>
-              {
-                val queue1 = queue.enqueue(output.message)
-                if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
-              })
-      }
-    }
-
-    private val timer = new Timer("receiver", true)
-    timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
-
-    def shutdown() { timer.cancel(); flush() }
-  }
-
-
   /* postponed changes */
 
   private object postponed_changes
@@ -521,10 +482,26 @@
       case arg: Any =>
         //{{{
         arg match {
+          case output: Prover.Output =>
+            if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
+            else handle_output(output)
+            if (output.is_syslog) {
+              syslog.change(queue =>
+                {
+                  val queue1 = queue.enqueue(output.message)
+                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
+                })
+              syslog_messages.post(output)
+            }
+            all_messages.post(output)
+
+          case input: Prover.Input =>
+            all_messages.post(input)
+
           case Start(name, args) if prover.isEmpty =>
             if (phase == Session.Inactive || phase == Session.Failed) {
               phase = Session.Startup
-              prover = Some(resources.start_prover(receiver.invoke _, name, args))
+              prover = Some(resources.start_prover(manager.send(_), name, args))
             }
 
           case Stop =>
@@ -555,18 +532,6 @@
           case Protocol_Command(name, args) if prover.isDefined =>
             prover.get.protocol_command(name, args:_*)
 
-          case Messages(msgs) =>
-            msgs foreach {
-              case input: Prover.Input =>
-                all_messages.post(input)
-
-              case output: Prover.Output =>
-                if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
-                else handle_output(output)
-                if (output.is_syslog) syslog_messages.post(output)
-                all_messages.post(output)
-            }
-
           case change: Session.Change if prover.isDefined =>
             if (global_state.value.is_assigned(change.previous))
               handle_change(change)
@@ -586,7 +551,6 @@
   def stop()
   {
     manager.send_wait(Stop)
-    receiver.shutdown()
     change_parser.shutdown()
     change_buffer.shutdown()
     manager.shutdown()
diff -r da3fefcb43c3 -r f7700146678d src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML	Fri Apr 25 23:29:54 2014 +0200
+++ b/src/Pure/System/message_channel.ML	Fri Apr 25 23:42:25 2014 +0200
@@ -34,14 +34,6 @@
   List.app (System_Channel.output channel) ss;
 
 
-(* flush *)
-
-fun flush channel = ignore (try System_Channel.flush channel);
-
-val flush_message = message Markup.protocolN Markup.flush [];
-fun flush_output channel = (output_message channel flush_message; flush channel);
-
-
 (* channel *)
 
 datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit};
@@ -49,15 +41,17 @@
 fun send (Message_Channel {send, ...}) = send;
 fun shutdown (Message_Channel {shutdown, ...}) = shutdown ();
 
+fun flush channel = ignore (try System_Channel.flush channel);
+
 fun message_output mbox channel =
   let
     fun loop receive =
       (case receive mbox of
-        SOME NONE => flush_output channel
+        SOME NONE => flush channel
       | SOME (SOME msg) =>
          (output_message channel msg;
           loop (Mailbox.receive_timeout (seconds 0.02)))
-      | NONE => (flush_output channel; loop (SOME o Mailbox.receive)));
+      | NONE => (flush channel; loop (SOME o Mailbox.receive)));
   in fn () => loop (SOME o Mailbox.receive) end;
 
 fun make channel =