# HG changeset patch # User huffman # Date 1315267500 25200 # Node ID 32e22fda8c702f99e7da98d44da643c355966241 # Parent 86f43cca4886840e00ff16ccfd67ddf0c3a7ed4e# Parent 81f683feaead6397866cd516668395d25474b2b3 merged diff -r 86f43cca4886 -r 32e22fda8c70 src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Mon Sep 05 17:00:56 2011 -0700 +++ b/src/Pure/PIDE/xml.scala Mon Sep 05 17:05:00 2011 -0700 @@ -11,7 +11,6 @@ import java.lang.ref.WeakReference import javax.xml.parsers.DocumentBuilderFactory -import scala.actors.Actor._ import scala.collection.mutable diff -r 86f43cca4886 -r 32e22fda8c70 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Mon Sep 05 17:00:56 2011 -0700 +++ b/src/Pure/System/session.scala Mon Sep 05 17:05:00 2011 -0700 @@ -10,7 +10,6 @@ import java.lang.System import scala.actors.TIMEOUT -import scala.actors.Actor import scala.actors.Actor._ @@ -62,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) } } } @@ -185,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) @@ -237,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) } //}}} @@ -297,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) @@ -362,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 @@ -421,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 } diff -r 86f43cca4886 -r 32e22fda8c70 src/Tools/jEdit/src/isabelle_markup.scala --- a/src/Tools/jEdit/src/isabelle_markup.scala Mon Sep 05 17:00:56 2011 -0700 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Mon Sep 05 17:05:00 2011 -0700 @@ -24,7 +24,6 @@ def get_color(s: String): Color = ColorFactory.getInstance.getColor(s) val outdated_color = new Color(238, 227, 227) - val outdated1_color = new Color(238, 227, 227, 50) val running_color = new Color(97, 0, 97) val running1_color = new Color(97, 0, 97, 100) val unfinished_color = new Color(255, 160, 160) @@ -57,7 +56,7 @@ def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] = { val state = snapshot.command_state(command) - if (snapshot.is_outdated) Some(outdated1_color) + if (snapshot.is_outdated) Some(outdated_color) else Isar_Document.command_status(state.status) match { case Isar_Document.Forked(i) if i > 0 => Some(running1_color) diff -r 86f43cca4886 -r 32e22fda8c70 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Mon Sep 05 17:00:56 2011 -0700 +++ b/src/Tools/jEdit/src/plugin.scala Mon Sep 05 17:05:00 2011 -0700 @@ -27,8 +27,7 @@ import org.gjt.sp.util.SyntaxUtilities import org.gjt.sp.util.Log -import scala.actors.Actor -import Actor._ +import scala.actors.Actor._ object Isabelle