manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);
authorwenzelm
Fri Apr 25 23:42:25 2014 +0200 (2014-04-25 ago)
changeset 56733f7700146678d
parent 56732 da3fefcb43c3
child 56734 6ca87a061740
manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/session.scala
src/Pure/System/message_channel.ML
     1.1 --- a/src/Pure/PIDE/markup.ML	Fri Apr 25 23:29:54 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Fri Apr 25 23:42:25 2014 +0200
     1.3 @@ -172,7 +172,6 @@
     1.4    val padding_command: Properties.entry
     1.5    val dialogN: string val dialog: serial -> string -> T
     1.6    val functionN: string
     1.7 -  val flush: Properties.T
     1.8    val assign_update: Properties.T
     1.9    val removed_versions: Properties.T
    1.10    val protocol_handler: string -> Properties.T
    1.11 @@ -557,8 +556,6 @@
    1.12  
    1.13  val functionN = "function"
    1.14  
    1.15 -val flush = [(functionN, "flush")];
    1.16 -
    1.17  val assign_update = [(functionN, "assign_update")];
    1.18  val removed_versions = [(functionN, "removed_versions")];
    1.19  
     2.1 --- a/src/Pure/PIDE/markup.scala	Fri Apr 25 23:29:54 2014 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Fri Apr 25 23:42:25 2014 +0200
     2.3 @@ -365,8 +365,6 @@
     2.4    val FUNCTION = "function"
     2.5    val Function = new Properties.String(FUNCTION)
     2.6  
     2.7 -  val Flush: Properties.T = List((FUNCTION, "flush"))
     2.8 -
     2.9    val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
    2.10    val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
    2.11  
     3.1 --- a/src/Pure/PIDE/session.scala	Fri Apr 25 23:29:54 2014 +0200
     3.2 +++ b/src/Pure/PIDE/session.scala	Fri Apr 25 23:42:25 2014 +0200
     3.3 @@ -261,7 +261,6 @@
     3.4    private case object Stop
     3.5    private case class Cancel_Exec(exec_id: Document_ID.Exec)
     3.6    private case class Protocol_Command(name: String, args: List[String])
     3.7 -  private case class Messages(msgs: List[Prover.Message])
     3.8    private case class Update_Options(options: Options)
     3.9  
    3.10  
    3.11 @@ -300,44 +299,6 @@
    3.12    }
    3.13  
    3.14  
    3.15 -  /* buffered prover messages */
    3.16 -
    3.17 -  private object receiver
    3.18 -  {
    3.19 -    private var buffer = new mutable.ListBuffer[Prover.Message]
    3.20 -
    3.21 -    private def flush(): Unit = synchronized {
    3.22 -      if (!buffer.isEmpty) {
    3.23 -        val msgs = buffer.toList
    3.24 -        manager.send(Messages(msgs))
    3.25 -        buffer = new mutable.ListBuffer[Prover.Message]
    3.26 -      }
    3.27 -    }
    3.28 -
    3.29 -    def invoke(msg: Prover.Message): Unit = synchronized {
    3.30 -      msg match {
    3.31 -        case _: Prover.Input =>
    3.32 -          buffer += msg
    3.33 -        case output: Prover.Protocol_Output if output.properties == Markup.Flush =>
    3.34 -          flush()
    3.35 -        case output: Prover.Output =>
    3.36 -          buffer += msg
    3.37 -          if (output.is_syslog)
    3.38 -            syslog.change(queue =>
    3.39 -              {
    3.40 -                val queue1 = queue.enqueue(output.message)
    3.41 -                if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
    3.42 -              })
    3.43 -      }
    3.44 -    }
    3.45 -
    3.46 -    private val timer = new Timer("receiver", true)
    3.47 -    timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
    3.48 -
    3.49 -    def shutdown() { timer.cancel(); flush() }
    3.50 -  }
    3.51 -
    3.52 -
    3.53    /* postponed changes */
    3.54  
    3.55    private object postponed_changes
    3.56 @@ -521,10 +482,26 @@
    3.57        case arg: Any =>
    3.58          //{{{
    3.59          arg match {
    3.60 +          case output: Prover.Output =>
    3.61 +            if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
    3.62 +            else handle_output(output)
    3.63 +            if (output.is_syslog) {
    3.64 +              syslog.change(queue =>
    3.65 +                {
    3.66 +                  val queue1 = queue.enqueue(output.message)
    3.67 +                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
    3.68 +                })
    3.69 +              syslog_messages.post(output)
    3.70 +            }
    3.71 +            all_messages.post(output)
    3.72 +
    3.73 +          case input: Prover.Input =>
    3.74 +            all_messages.post(input)
    3.75 +
    3.76            case Start(name, args) if prover.isEmpty =>
    3.77              if (phase == Session.Inactive || phase == Session.Failed) {
    3.78                phase = Session.Startup
    3.79 -              prover = Some(resources.start_prover(receiver.invoke _, name, args))
    3.80 +              prover = Some(resources.start_prover(manager.send(_), name, args))
    3.81              }
    3.82  
    3.83            case Stop =>
    3.84 @@ -555,18 +532,6 @@
    3.85            case Protocol_Command(name, args) if prover.isDefined =>
    3.86              prover.get.protocol_command(name, args:_*)
    3.87  
    3.88 -          case Messages(msgs) =>
    3.89 -            msgs foreach {
    3.90 -              case input: Prover.Input =>
    3.91 -                all_messages.post(input)
    3.92 -
    3.93 -              case output: Prover.Output =>
    3.94 -                if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
    3.95 -                else handle_output(output)
    3.96 -                if (output.is_syslog) syslog_messages.post(output)
    3.97 -                all_messages.post(output)
    3.98 -            }
    3.99 -
   3.100            case change: Session.Change if prover.isDefined =>
   3.101              if (global_state.value.is_assigned(change.previous))
   3.102                handle_change(change)
   3.103 @@ -586,7 +551,6 @@
   3.104    def stop()
   3.105    {
   3.106      manager.send_wait(Stop)
   3.107 -    receiver.shutdown()
   3.108      change_parser.shutdown()
   3.109      change_buffer.shutdown()
   3.110      manager.shutdown()
     4.1 --- a/src/Pure/System/message_channel.ML	Fri Apr 25 23:29:54 2014 +0200
     4.2 +++ b/src/Pure/System/message_channel.ML	Fri Apr 25 23:42:25 2014 +0200
     4.3 @@ -34,14 +34,6 @@
     4.4    List.app (System_Channel.output channel) ss;
     4.5  
     4.6  
     4.7 -(* flush *)
     4.8 -
     4.9 -fun flush channel = ignore (try System_Channel.flush channel);
    4.10 -
    4.11 -val flush_message = message Markup.protocolN Markup.flush [];
    4.12 -fun flush_output channel = (output_message channel flush_message; flush channel);
    4.13 -
    4.14 -
    4.15  (* channel *)
    4.16  
    4.17  datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit};
    4.18 @@ -49,15 +41,17 @@
    4.19  fun send (Message_Channel {send, ...}) = send;
    4.20  fun shutdown (Message_Channel {shutdown, ...}) = shutdown ();
    4.21  
    4.22 +fun flush channel = ignore (try System_Channel.flush channel);
    4.23 +
    4.24  fun message_output mbox channel =
    4.25    let
    4.26      fun loop receive =
    4.27        (case receive mbox of
    4.28 -        SOME NONE => flush_output channel
    4.29 +        SOME NONE => flush channel
    4.30        | SOME (SOME msg) =>
    4.31           (output_message channel msg;
    4.32            loop (Mailbox.receive_timeout (seconds 0.02)))
    4.33 -      | NONE => (flush_output channel; loop (SOME o Mailbox.receive)));
    4.34 +      | NONE => (flush channel; loop (SOME o Mailbox.receive)));
    4.35    in fn () => loop (SOME o Mailbox.receive) end;
    4.36  
    4.37  fun make channel =