commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
authorwenzelm
Mon Sep 05 23:26:41 2011 +0200 (2011-09-05)
changeset 44722a8331fb5c959
parent 44721 ba478c3f7255
child 44723 81f683feaead
commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
src/Pure/System/session.scala
     1.1 --- a/src/Pure/System/session.scala	Mon Sep 05 20:30:37 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Mon Sep 05 23:26:41 2011 +0200
     1.3 @@ -61,49 +61,15 @@
     1.4    //{{{
     1.5    private case object Stop
     1.6  
     1.7 -  private val (_, command_change_buffer) =
     1.8 -    Simple_Thread.actor("command_change_buffer", daemon = true)
     1.9 +  private val (_, commands_changed_buffer) =
    1.10 +    Simple_Thread.actor("commands_changed_buffer", daemon = true)
    1.11    {
    1.12 -    var changed_nodes: Set[Document.Node.Name] = Set.empty
    1.13 -    var changed_commands: Set[Command] = Set.empty
    1.14 -    def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
    1.15 -
    1.16 -    var flush_time: Option[Long] = None
    1.17 -
    1.18 -    def flush_timeout: Long =
    1.19 -      flush_time match {
    1.20 -        case None => 5000L
    1.21 -        case Some(time) => (time - System.currentTimeMillis()) max 0
    1.22 -      }
    1.23 -
    1.24 -    def flush()
    1.25 -    {
    1.26 -      if (changed)
    1.27 -        commands_changed.event(Session.Commands_Changed(changed_nodes, changed_commands))
    1.28 -      changed_nodes = Set.empty
    1.29 -      changed_commands = Set.empty
    1.30 -      flush_time = None
    1.31 -    }
    1.32 -
    1.33 -    def invoke()
    1.34 -    {
    1.35 -      val now = System.currentTimeMillis()
    1.36 -      flush_time match {
    1.37 -        case None => flush_time = Some(now + output_delay.ms)
    1.38 -        case Some(time) => if (now >= time) flush()
    1.39 -      }
    1.40 -    }
    1.41 -
    1.42      var finished = false
    1.43      while (!finished) {
    1.44 -      receiveWithin(flush_timeout) {
    1.45 -        case command: Command =>
    1.46 -          changed_nodes += command.node_name
    1.47 -          changed_commands += command
    1.48 -          invoke()
    1.49 -        case TIMEOUT => flush()
    1.50 +      receive {
    1.51          case Stop => finished = true; reply(())
    1.52 -        case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
    1.53 +        case changed: Session.Commands_Changed => commands_changed.event(changed)
    1.54 +        case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
    1.55        }
    1.56      }
    1.57    }
    1.58 @@ -184,6 +150,44 @@
    1.59      var prune_next = System.currentTimeMillis() + prune_delay.ms
    1.60  
    1.61  
    1.62 +    /* delayed command changes */
    1.63 +
    1.64 +    object commands_changed_delay
    1.65 +    {
    1.66 +      private var changed_nodes: Set[Document.Node.Name] = Set.empty
    1.67 +      private var changed_commands: Set[Command] = Set.empty
    1.68 +      private def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
    1.69 +
    1.70 +      private var flush_time: Option[Long] = None
    1.71 +
    1.72 +      def flush_timeout: Long =
    1.73 +        flush_time match {
    1.74 +          case None => 5000L
    1.75 +          case Some(time) => (time - System.currentTimeMillis()) max 0
    1.76 +        }
    1.77 +
    1.78 +      def flush()
    1.79 +      {
    1.80 +        if (changed)
    1.81 +          commands_changed_buffer ! Session.Commands_Changed(changed_nodes, changed_commands)
    1.82 +        changed_nodes = Set.empty
    1.83 +        changed_commands = Set.empty
    1.84 +        flush_time = None
    1.85 +      }
    1.86 +
    1.87 +      def invoke(command: Command)
    1.88 +      {
    1.89 +        changed_nodes += command.node_name
    1.90 +        changed_commands += command
    1.91 +        val now = System.currentTimeMillis()
    1.92 +        flush_time match {
    1.93 +          case None => flush_time = Some(now + output_delay.ms)
    1.94 +          case Some(time) => if (now >= time) flush()
    1.95 +        }
    1.96 +      }
    1.97 +    }
    1.98 +
    1.99 +
   1.100      /* perspective */
   1.101  
   1.102      def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
   1.103 @@ -236,7 +240,7 @@
   1.104      //{{{
   1.105      {
   1.106        val cmds = global_state.change_yield(_.assign(id, assign))
   1.107 -      for (cmd <- cmds) command_change_buffer ! cmd
   1.108 +      for (cmd <- cmds) commands_changed_delay.invoke(cmd)
   1.109        assignments.event(Session.Assignment)
   1.110      }
   1.111      //}}}
   1.112 @@ -296,7 +300,7 @@
   1.113          case Position.Id(state_id) if !result.is_raw =>
   1.114            try {
   1.115              val st = global_state.change_yield(_.accumulate(state_id, result.message))
   1.116 -            command_change_buffer ! st.command
   1.117 +            commands_changed_delay.invoke(st.command)
   1.118            }
   1.119            catch {
   1.120              case _: Document.State.Fail => bad_result(result)
   1.121 @@ -361,7 +365,9 @@
   1.122      //{{{
   1.123      var finished = false
   1.124      while (!finished) {
   1.125 -      receive {
   1.126 +      receiveWithin(commands_changed_delay.flush_timeout) {
   1.127 +        case TIMEOUT => commands_changed_delay.flush()
   1.128 +
   1.129          case Start(timeout, args) if prover.isEmpty =>
   1.130            if (phase == Session.Inactive || phase == Session.Failed) {
   1.131              phase = Session.Startup
   1.132 @@ -420,7 +426,7 @@
   1.133  
   1.134    def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
   1.135  
   1.136 -  def stop() { command_change_buffer !? Stop; session_actor !? Stop }
   1.137 +  def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
   1.138  
   1.139    def interrupt() { session_actor ! Interrupt }
   1.140