1.1 --- a/src/Pure/Concurrent/volatile.scala Sun Feb 26 19:20:46 2012 +0100
1.2 +++ b/src/Pure/Concurrent/volatile.scala Sun Feb 26 19:36:35 2012 +0100
1.3 @@ -18,8 +18,8 @@
1.4 {
1.5 @volatile private var state: A = init
1.6 def apply(): A = state
1.7 - def change(f: A => A) { state = f(state) }
1.8 - def change_yield[B](f: A => (B, A)): B =
1.9 + def >> (f: A => A) { state = f(state) }
1.10 + def >>>[B] (f: A => (B, A)): B =
1.11 {
1.12 val (result, new_state) = f(state)
1.13 state = new_state
2.1 --- a/src/Pure/System/session.scala Sun Feb 26 19:20:46 2012 +0100
2.2 +++ b/src/Pure/System/session.scala Sun Feb 26 19:36:35 2012 +0100
2.3 @@ -262,12 +262,12 @@
2.4 val text_edits: List[Document.Edit_Text] =
2.5 List((name, Document.Node.Perspective(text_perspective)))
2.6 val change =
2.7 - global_state.change_yield(
2.8 - _.continue_history(Future.value(previous), text_edits, Future.value(version)))
2.9 + global_state >>>
2.10 + (_.continue_history(Future.value(previous), text_edits, Future.value(version)))
2.11
2.12 val assignment = global_state().the_assignment(previous).check_finished
2.13 - global_state.change(_.define_version(version, assignment))
2.14 - global_state.change_yield(_.assign(version.id))
2.15 + global_state >> (_.define_version(version, assignment))
2.16 + global_state >>> (_.assign(version.id))
2.17
2.18 prover.get.update_perspective(previous.id, version.id, name, perspective)
2.19 }
2.20 @@ -286,7 +286,7 @@
2.21
2.22 val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
2.23 val version = Future.promise[Document.Version]
2.24 - val change = global_state.change_yield(_.continue_history(previous, text_edits, version))
2.25 + val change = global_state >>> (_.continue_history(previous, text_edits, version))
2.26
2.27 change_parser ! Text_Edits(syntax, name, previous, text_edits, version)
2.28 }
2.29 @@ -298,7 +298,7 @@
2.30 def handle_assign(id: Document.Version_ID, assign: Document.Assign)
2.31 //{{{
2.32 {
2.33 - val cmds = global_state.change_yield(_.assign(id, assign))
2.34 + val cmds = global_state >>> (_.assign(id, assign))
2.35 for (cmd <- cmds) delay_commands_changed.invoke(cmd)
2.36 }
2.37 //}}}
2.38 @@ -309,7 +309,7 @@
2.39 def handle_removed(removed: List[Document.Version_ID])
2.40 //{{{
2.41 {
2.42 - global_state.change(_.removed_versions(removed))
2.43 + global_state >> (_.removed_versions(removed))
2.44 }
2.45 //}}}
2.46
2.47 @@ -327,7 +327,7 @@
2.48 def id_command(command: Command)
2.49 {
2.50 if (!global_state().defined_command(command.id)) {
2.51 - global_state.change(_.define_command(command))
2.52 + global_state >> (_.define_command(command))
2.53 prover.get.define_command(command)
2.54 }
2.55 }
2.56 @@ -337,7 +337,7 @@
2.57 }
2.58
2.59 val assignment = global_state().the_assignment(previous).check_finished
2.60 - global_state.change(_.define_version(version, assignment))
2.61 + global_state >> (_.define_version(version, assignment))
2.62 prover.get.update(previous.id, version.id, doc_edits)
2.63 }
2.64 //}}}
2.65 @@ -358,7 +358,7 @@
2.66
2.67 case Position.Id(state_id) if !result.is_raw =>
2.68 try {
2.69 - val st = global_state.change_yield(_.accumulate(state_id, result.message))
2.70 + val st = global_state >>> (_.accumulate(state_id, result.message))
2.71 delay_commands_changed.invoke(st.command)
2.72 }
2.73 catch {
2.74 @@ -374,7 +374,7 @@
2.75 }
2.76 // FIXME separate timeout event/message!?
2.77 if (prover.isDefined && System.currentTimeMillis() > prune_next) {
2.78 - val old_versions = global_state.change_yield(_.prune_history(prune_size))
2.79 + val old_versions = global_state >>> (_.prune_history(prune_size))
2.80 if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
2.81 prune_next = System.currentTimeMillis() + prune_delay.ms
2.82 }
2.83 @@ -441,7 +441,7 @@
2.84
2.85 case Stop =>
2.86 if (phase == Session.Ready) {
2.87 - global_state.change(_ => Document.State.init) // FIXME event bus!?
2.88 + global_state >> (_ => Document.State.init) // FIXME event bus!?
2.89 phase = Session.Shutdown
2.90 prover.get.terminate
2.91 prover = None