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