--- 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
--- 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 }
--- 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)
--- 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