# HG changeset patch # User wenzelm # Date 1315258001 -7200 # Node ID a8331fb5c959de8f037cf1985281f84bae4f9e6f # Parent ba478c3f7255440b6a750684533e89a08cf4e69f commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel; diff -r ba478c3f7255 -r a8331fb5c959 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Mon Sep 05 20:30:37 2011 +0200 +++ b/src/Pure/System/session.scala Mon Sep 05 23:26:41 2011 +0200 @@ -61,49 +61,15 @@ //{{{ private case object Stop - private val (_, command_change_buffer) = - Simple_Thread.actor("command_change_buffer", daemon = true) + private val (_, commands_changed_buffer) = + Simple_Thread.actor("commands_changed_buffer", daemon = true) { - var changed_nodes: Set[Document.Node.Name] = Set.empty - var changed_commands: Set[Command] = Set.empty - def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty - - var flush_time: Option[Long] = None - - def flush_timeout: Long = - flush_time match { - case None => 5000L - case Some(time) => (time - System.currentTimeMillis()) max 0 - } - - def flush() - { - if (changed) - commands_changed.event(Session.Commands_Changed(changed_nodes, changed_commands)) - changed_nodes = Set.empty - changed_commands = Set.empty - flush_time = None - } - - def invoke() - { - val now = System.currentTimeMillis() - flush_time match { - case None => flush_time = Some(now + output_delay.ms) - case Some(time) => if (now >= time) flush() - } - } - var finished = false while (!finished) { - receiveWithin(flush_timeout) { - case command: Command => - changed_nodes += command.node_name - changed_commands += command - invoke() - case TIMEOUT => flush() + receive { case Stop => finished = true; reply(()) - case bad => System.err.println("command_change_buffer: ignoring bad message " + bad) + case changed: Session.Commands_Changed => commands_changed.event(changed) + case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad) } } } @@ -184,6 +150,44 @@ var prune_next = System.currentTimeMillis() + prune_delay.ms + /* delayed command changes */ + + object commands_changed_delay + { + private var changed_nodes: Set[Document.Node.Name] = Set.empty + private var changed_commands: Set[Command] = Set.empty + private def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty + + private var flush_time: Option[Long] = None + + def flush_timeout: Long = + flush_time match { + case None => 5000L + case Some(time) => (time - System.currentTimeMillis()) max 0 + } + + def flush() + { + if (changed) + commands_changed_buffer ! Session.Commands_Changed(changed_nodes, changed_commands) + changed_nodes = Set.empty + changed_commands = Set.empty + flush_time = None + } + + def invoke(command: Command) + { + changed_nodes += command.node_name + changed_commands += command + val now = System.currentTimeMillis() + flush_time match { + case None => flush_time = Some(now + output_delay.ms) + case Some(time) => if (now >= time) flush() + } + } + } + + /* perspective */ def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective) @@ -236,7 +240,7 @@ //{{{ { val cmds = global_state.change_yield(_.assign(id, assign)) - for (cmd <- cmds) command_change_buffer ! cmd + for (cmd <- cmds) commands_changed_delay.invoke(cmd) assignments.event(Session.Assignment) } //}}} @@ -296,7 +300,7 @@ case Position.Id(state_id) if !result.is_raw => try { val st = global_state.change_yield(_.accumulate(state_id, result.message)) - command_change_buffer ! st.command + commands_changed_delay.invoke(st.command) } catch { case _: Document.State.Fail => bad_result(result) @@ -361,7 +365,9 @@ //{{{ var finished = false while (!finished) { - receive { + receiveWithin(commands_changed_delay.flush_timeout) { + case TIMEOUT => commands_changed_delay.flush() + case Start(timeout, args) if prover.isEmpty => if (phase == Session.Inactive || phase == Session.Failed) { phase = Session.Startup @@ -420,7 +426,7 @@ def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) } - def stop() { command_change_buffer !? Stop; session_actor !? Stop } + def stop() { commands_changed_buffer !? Stop; session_actor !? Stop } def interrupt() { session_actor ! Interrupt }