src/Pure/PIDE/session.scala
changeset 56719 80eb2192516a
parent 56715 52125652e82a
child 56733 f7700146678d
     1.1 --- a/src/Pure/PIDE/session.scala	Fri Apr 25 13:29:56 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Fri Apr 25 13:55:50 2014 +0200
     1.3 @@ -182,46 +182,6 @@
     1.4  
     1.5  
     1.6  
     1.7 -  /** buffered changes: to be dispatched to clients **/
     1.8 -
     1.9 -  private case class Received_Change(assignment: Boolean, commands: List[Command])
    1.10 -
    1.11 -  private val change_buffer: Consumer_Thread[Received_Change] =
    1.12 -  {
    1.13 -    object changed
    1.14 -    {
    1.15 -      private var assignment: Boolean = false
    1.16 -      private var nodes: Set[Document.Node.Name] = Set.empty
    1.17 -      private var commands: Set[Command] = Set.empty
    1.18 -
    1.19 -      def flush(): Unit = synchronized {
    1.20 -        if (assignment || !nodes.isEmpty || !commands.isEmpty)
    1.21 -          commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
    1.22 -        assignment = false
    1.23 -        nodes = Set.empty
    1.24 -        commands = Set.empty
    1.25 -      }
    1.26 -
    1.27 -      def invoke(change: Received_Change): Unit = synchronized {
    1.28 -        assignment |= change.assignment
    1.29 -        for (command <- change.commands) {
    1.30 -          nodes += command.node_name
    1.31 -          commands += command
    1.32 -        }
    1.33 -      }
    1.34 -    }
    1.35 -
    1.36 -    val timer = new Timer("change_buffer", true)
    1.37 -    timer.schedule(new TimerTask { def run = changed.flush() }, output_delay.ms, output_delay.ms)
    1.38 -
    1.39 -    Consumer_Thread.fork[Received_Change]("change_buffer", daemon = true)(
    1.40 -      consume = { case change => changed.invoke(change); true },
    1.41 -      finish = () => { timer.cancel(); changed.flush() }
    1.42 -    )
    1.43 -  }
    1.44 -
    1.45 -
    1.46 -
    1.47    /** pipelined change parsing **/
    1.48  
    1.49    private case class Text_Edits(
    1.50 @@ -305,6 +265,41 @@
    1.51    private case class Update_Options(options: Options)
    1.52  
    1.53  
    1.54 +  /* buffered changes */
    1.55 +
    1.56 +  private object change_buffer
    1.57 +  {
    1.58 +    private var assignment: Boolean = false
    1.59 +    private var nodes: Set[Document.Node.Name] = Set.empty
    1.60 +    private var commands: Set[Command] = Set.empty
    1.61 +
    1.62 +    def flush(): Unit = synchronized {
    1.63 +      if (assignment || !nodes.isEmpty || !commands.isEmpty)
    1.64 +        commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
    1.65 +      assignment = false
    1.66 +      nodes = Set.empty
    1.67 +      commands = Set.empty
    1.68 +    }
    1.69 +
    1.70 +    def invoke(assign: Boolean, cmds: List[Command]): Unit = synchronized {
    1.71 +      assignment |= assign
    1.72 +      for (command <- cmds) {
    1.73 +        nodes += command.node_name
    1.74 +        commands += command
    1.75 +      }
    1.76 +    }
    1.77 +
    1.78 +    private val timer = new Timer("change_buffer", true)
    1.79 +    timer.schedule(new TimerTask { def run = flush() }, output_delay.ms, output_delay.ms)
    1.80 +
    1.81 +    def shutdown()
    1.82 +    {
    1.83 +      timer.cancel()
    1.84 +      flush()
    1.85 +    }
    1.86 +  }
    1.87 +
    1.88 +
    1.89    /* buffered prover messages */
    1.90  
    1.91    private object receiver
    1.92 @@ -443,7 +438,7 @@
    1.93        {
    1.94          try {
    1.95            val st = global_state.change_result(_.accumulate(state_id, message))
    1.96 -          change_buffer.send(Received_Change(false, List(st.command)))
    1.97 +          change_buffer.invoke(false, List(st.command))
    1.98          }
    1.99          catch {
   1.100            case _: Document.State.Fail => bad_output()
   1.101 @@ -467,7 +462,7 @@
   1.102                    case Protocol.Assign_Update(id, update) =>
   1.103                      try {
   1.104                        val cmds = global_state.change_result(_.assign(id, update))
   1.105 -                      change_buffer.send(Received_Change(true, cmds))
   1.106 +                      change_buffer.invoke(true, cmds)
   1.107                      }
   1.108                      catch { case _: Document.State.Fail => bad_output() }
   1.109                      postponed_changes.flush()