merged
authorhuffman
Mon Sep 05 17:05:00 2011 -0700 (2011-09-05)
changeset 4472932e22fda8c70
parent 44728 86f43cca4886
parent 44723 81f683feaead
child 44730 11a1290fd0ac
merged
     1.1 --- a/src/Pure/PIDE/xml.scala	Mon Sep 05 17:00:56 2011 -0700
     1.2 +++ b/src/Pure/PIDE/xml.scala	Mon Sep 05 17:05:00 2011 -0700
     1.3 @@ -11,7 +11,6 @@
     1.4  import java.lang.ref.WeakReference
     1.5  import javax.xml.parsers.DocumentBuilderFactory
     1.6  
     1.7 -import scala.actors.Actor._
     1.8  import scala.collection.mutable
     1.9  
    1.10  
     2.1 --- a/src/Pure/System/session.scala	Mon Sep 05 17:00:56 2011 -0700
     2.2 +++ b/src/Pure/System/session.scala	Mon Sep 05 17:05:00 2011 -0700
     2.3 @@ -10,7 +10,6 @@
     2.4  import java.lang.System
     2.5  
     2.6  import scala.actors.TIMEOUT
     2.7 -import scala.actors.Actor
     2.8  import scala.actors.Actor._
     2.9  
    2.10  
    2.11 @@ -62,49 +61,15 @@
    2.12    //{{{
    2.13    private case object Stop
    2.14  
    2.15 -  private val (_, command_change_buffer) =
    2.16 -    Simple_Thread.actor("command_change_buffer", daemon = true)
    2.17 +  private val (_, commands_changed_buffer) =
    2.18 +    Simple_Thread.actor("commands_changed_buffer", daemon = true)
    2.19    {
    2.20 -    var changed_nodes: Set[Document.Node.Name] = Set.empty
    2.21 -    var changed_commands: Set[Command] = Set.empty
    2.22 -    def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
    2.23 -
    2.24 -    var flush_time: Option[Long] = None
    2.25 -
    2.26 -    def flush_timeout: Long =
    2.27 -      flush_time match {
    2.28 -        case None => 5000L
    2.29 -        case Some(time) => (time - System.currentTimeMillis()) max 0
    2.30 -      }
    2.31 -
    2.32 -    def flush()
    2.33 -    {
    2.34 -      if (changed)
    2.35 -        commands_changed.event(Session.Commands_Changed(changed_nodes, changed_commands))
    2.36 -      changed_nodes = Set.empty
    2.37 -      changed_commands = Set.empty
    2.38 -      flush_time = None
    2.39 -    }
    2.40 -
    2.41 -    def invoke()
    2.42 -    {
    2.43 -      val now = System.currentTimeMillis()
    2.44 -      flush_time match {
    2.45 -        case None => flush_time = Some(now + output_delay.ms)
    2.46 -        case Some(time) => if (now >= time) flush()
    2.47 -      }
    2.48 -    }
    2.49 -
    2.50      var finished = false
    2.51      while (!finished) {
    2.52 -      receiveWithin(flush_timeout) {
    2.53 -        case command: Command =>
    2.54 -          changed_nodes += command.node_name
    2.55 -          changed_commands += command
    2.56 -          invoke()
    2.57 -        case TIMEOUT => flush()
    2.58 +      receive {
    2.59          case Stop => finished = true; reply(())
    2.60 -        case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
    2.61 +        case changed: Session.Commands_Changed => commands_changed.event(changed)
    2.62 +        case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
    2.63        }
    2.64      }
    2.65    }
    2.66 @@ -185,6 +150,44 @@
    2.67      var prune_next = System.currentTimeMillis() + prune_delay.ms
    2.68  
    2.69  
    2.70 +    /* delayed command changes */
    2.71 +
    2.72 +    object commands_changed_delay
    2.73 +    {
    2.74 +      private var changed_nodes: Set[Document.Node.Name] = Set.empty
    2.75 +      private var changed_commands: Set[Command] = Set.empty
    2.76 +      private def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
    2.77 +
    2.78 +      private var flush_time: Option[Long] = None
    2.79 +
    2.80 +      def flush_timeout: Long =
    2.81 +        flush_time match {
    2.82 +          case None => 5000L
    2.83 +          case Some(time) => (time - System.currentTimeMillis()) max 0
    2.84 +        }
    2.85 +
    2.86 +      def flush()
    2.87 +      {
    2.88 +        if (changed)
    2.89 +          commands_changed_buffer ! Session.Commands_Changed(changed_nodes, changed_commands)
    2.90 +        changed_nodes = Set.empty
    2.91 +        changed_commands = Set.empty
    2.92 +        flush_time = None
    2.93 +      }
    2.94 +
    2.95 +      def invoke(command: Command)
    2.96 +      {
    2.97 +        changed_nodes += command.node_name
    2.98 +        changed_commands += command
    2.99 +        val now = System.currentTimeMillis()
   2.100 +        flush_time match {
   2.101 +          case None => flush_time = Some(now + output_delay.ms)
   2.102 +          case Some(time) => if (now >= time) flush()
   2.103 +        }
   2.104 +      }
   2.105 +    }
   2.106 +
   2.107 +
   2.108      /* perspective */
   2.109  
   2.110      def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
   2.111 @@ -237,7 +240,7 @@
   2.112      //{{{
   2.113      {
   2.114        val cmds = global_state.change_yield(_.assign(id, assign))
   2.115 -      for (cmd <- cmds) command_change_buffer ! cmd
   2.116 +      for (cmd <- cmds) commands_changed_delay.invoke(cmd)
   2.117        assignments.event(Session.Assignment)
   2.118      }
   2.119      //}}}
   2.120 @@ -297,7 +300,7 @@
   2.121          case Position.Id(state_id) if !result.is_raw =>
   2.122            try {
   2.123              val st = global_state.change_yield(_.accumulate(state_id, result.message))
   2.124 -            command_change_buffer ! st.command
   2.125 +            commands_changed_delay.invoke(st.command)
   2.126            }
   2.127            catch {
   2.128              case _: Document.State.Fail => bad_result(result)
   2.129 @@ -362,7 +365,9 @@
   2.130      //{{{
   2.131      var finished = false
   2.132      while (!finished) {
   2.133 -      receive {
   2.134 +      receiveWithin(commands_changed_delay.flush_timeout) {
   2.135 +        case TIMEOUT => commands_changed_delay.flush()
   2.136 +
   2.137          case Start(timeout, args) if prover.isEmpty =>
   2.138            if (phase == Session.Inactive || phase == Session.Failed) {
   2.139              phase = Session.Startup
   2.140 @@ -421,7 +426,7 @@
   2.141  
   2.142    def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
   2.143  
   2.144 -  def stop() { command_change_buffer !? Stop; session_actor !? Stop }
   2.145 +  def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
   2.146  
   2.147    def interrupt() { session_actor ! Interrupt }
   2.148  
     3.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Mon Sep 05 17:00:56 2011 -0700
     3.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Mon Sep 05 17:05:00 2011 -0700
     3.3 @@ -24,7 +24,6 @@
     3.4    def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
     3.5  
     3.6    val outdated_color = new Color(238, 227, 227)
     3.7 -  val outdated1_color = new Color(238, 227, 227, 50)
     3.8    val running_color = new Color(97, 0, 97)
     3.9    val running1_color = new Color(97, 0, 97, 100)
    3.10    val unfinished_color = new Color(255, 160, 160)
    3.11 @@ -57,7 +56,7 @@
    3.12    def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    3.13    {
    3.14      val state = snapshot.command_state(command)
    3.15 -    if (snapshot.is_outdated) Some(outdated1_color)
    3.16 +    if (snapshot.is_outdated) Some(outdated_color)
    3.17      else
    3.18        Isar_Document.command_status(state.status) match {
    3.19          case Isar_Document.Forked(i) if i > 0 => Some(running1_color)
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Sep 05 17:00:56 2011 -0700
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Sep 05 17:05:00 2011 -0700
     4.3 @@ -27,8 +27,7 @@
     4.4  import org.gjt.sp.util.SyntaxUtilities
     4.5  import org.gjt.sp.util.Log
     4.6  
     4.7 -import scala.actors.Actor
     4.8 -import Actor._
     4.9 +import scala.actors.Actor._
    4.10  
    4.11  
    4.12  object Isabelle