1.1 --- a/src/Pure/System/session.scala	Tue Feb 21 13:10:13 2012 +0100
     1.2 +++ b/src/Pure/System/session.scala	Tue Feb 21 13:37:03 2012 +0100
     1.3 @@ -216,7 +216,7 @@
     1.4  
     1.5      /* delayed command changes */
     1.6  
     1.7 -    object commands_changed_delay
     1.8 +    object delay_commands_changed
     1.9      {
    1.10        private var changed_nodes: Set[Document.Node.Name] = Set.empty
    1.11        private var changed_commands: Set[Command] = Set.empty
    1.12 @@ -299,7 +299,7 @@
    1.13      //{{{
    1.14      {
    1.15        val cmds = global_state.change_yield(_.assign(id, assign))
    1.16 -      for (cmd <- cmds) commands_changed_delay.invoke(cmd)
    1.17 +      for (cmd <- cmds) delay_commands_changed.invoke(cmd)
    1.18      }
    1.19      //}}}
    1.20  
    1.21 @@ -359,7 +359,7 @@
    1.22          case Position.Id(state_id) if !result.is_raw =>
    1.23            try {
    1.24              val st = global_state.change_yield(_.accumulate(state_id, result.message))
    1.25 -            commands_changed_delay.invoke(st.command)
    1.26 +            delay_commands_changed.invoke(st.command)
    1.27            }
    1.28            catch {
    1.29              case _: Document.State.Fail => bad_result(result)
    1.30 @@ -430,8 +430,8 @@
    1.31      //{{{
    1.32      var finished = false
    1.33      while (!finished) {
    1.34 -      receiveWithin(commands_changed_delay.flush_timeout) {
    1.35 -        case TIMEOUT => commands_changed_delay.flush()
    1.36 +      receiveWithin(delay_commands_changed.flush_timeout) {
    1.37 +        case TIMEOUT => delay_commands_changed.flush()
    1.38  
    1.39          case Start(timeout, args) if prover.isEmpty =>
    1.40            if (phase == Session.Inactive || phase == Session.Failed) {