--- a/src/Pure/Concurrent/synchronized.scala Thu Apr 24 00:29:55 2014 +0200
+++ b/src/Pure/Concurrent/synchronized.scala Thu Apr 24 10:24:44 2014 +0200
@@ -17,9 +17,9 @@
final class Synchronized[A] private(init: A)
{
private var state: A = init
- def apply(): A = synchronized { state }
- def >> (f: A => A) = synchronized { state = f(state) }
- def >>>[B] (f: A => (B, A)): B = synchronized {
+ def value: A = synchronized { state }
+ def change(f: A => A) = synchronized { state = f(state) }
+ def change_result[B](f: A => (B, A)): B = synchronized {
val (result, new_state) = f(state)
state = new_state
result
--- a/src/Pure/Concurrent/volatile.scala Thu Apr 24 00:29:55 2014 +0200
+++ b/src/Pure/Concurrent/volatile.scala Thu Apr 24 10:24:44 2014 +0200
@@ -17,9 +17,9 @@
final class Volatile[A] private(init: A)
{
@volatile private var state: A = init
- def apply(): A = state
- def >> (f: A => A) { state = f(state) }
- def >>>[B] (f: A => (B, A)): B =
+ def value: A = state
+ def change(f: A => A) { state = f(state) }
+ def change_result[B](f: A => (B, A)): B =
{
val (result, new_state) = f(state)
state = new_state
--- a/src/Pure/PIDE/session.scala Thu Apr 24 00:29:55 2014 +0200
+++ b/src/Pure/PIDE/session.scala Thu Apr 24 10:24:44 2014 +0200
@@ -208,7 +208,7 @@
/* global state */
private val syslog = Volatile(Queue.empty[XML.Elem])
- def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content))
+ def current_syslog(): String = cat_lines(syslog.value.iterator.map(XML.content))
@volatile private var _phase: Session.Phase = Session.Inactive
private def phase_=(new_phase: Session.Phase)
@@ -220,7 +220,7 @@
def is_ready: Boolean = phase == Session.Ready
private val global_state = Volatile(Document.State.init)
- def current_state(): Document.State = global_state()
+ def current_state(): Document.State = global_state.value
def recent_syntax(): Prover.Syntax =
{
@@ -230,7 +230,7 @@
def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
- global_state().snapshot(name, pending_edits)
+ global_state.value.snapshot(name, pending_edits)
/* protocol handlers */
@@ -290,7 +290,7 @@
case output: Prover.Output =>
buffer += msg
if (output.is_syslog)
- syslog >> (queue =>
+ syslog.change(queue =>
{
val queue1 = queue.enqueue(output.message)
if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
@@ -357,9 +357,9 @@
{
prover.get.discontinue_execution()
- val previous = global_state().history.tip.version
+ val previous = global_state.value.history.tip.version
val version = Future.promise[Document.Version]
- val change = global_state >>> (_.continue_history(previous, edits, version))
+ val change = global_state.change_result(_.continue_history(previous, edits, version))
raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
change_parser ! Text_Edits(previous, doc_blobs, edits, version)
@@ -376,19 +376,19 @@
{
for {
digest <- command.blobs_digests
- if !global_state().defined_blob(digest)
+ if !global_state.value.defined_blob(digest)
} {
change.doc_blobs.get(digest) match {
case Some(blob) =>
- global_state >> (_.define_blob(digest))
+ global_state.change(_.define_blob(digest))
prover.get.define_blob(digest, blob.bytes)
case None =>
System.err.println("Missing blob for SHA1 digest " + digest)
}
}
- if (!global_state().defined_command(command.id)) {
- global_state >> (_.define_command(command))
+ if (!global_state.value.defined_command(command.id)) {
+ global_state.change(_.define_command(command))
prover.get.define_command(command)
}
}
@@ -397,8 +397,8 @@
edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
}
- val assignment = global_state().the_assignment(change.previous).check_finished
- global_state >> (_.define_version(change.version, assignment))
+ val assignment = global_state.value.the_assignment(change.previous).check_finished
+ global_state.change(_.define_version(change.version, assignment))
prover.get.update(change.previous.id, change.version.id, change.doc_edits)
resources.commit(change)
}
@@ -419,7 +419,7 @@
def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
{
try {
- val st = global_state >>> (_.accumulate(state_id, message))
+ val st = global_state.change_result(_.accumulate(state_id, message))
delay_commands_changed.invoke(false, List(st.command))
}
catch {
@@ -443,7 +443,7 @@
msg.text match {
case Protocol.Assign_Update(id, update) =>
try {
- val cmds = global_state >>> (_.assign(id, update))
+ val cmds = global_state.change_result(_.assign(id, update))
delay_commands_changed.invoke(true, cmds)
}
catch { case _: Document.State.Fail => bad_output() }
@@ -451,7 +451,7 @@
}
// FIXME separate timeout event/message!?
if (prover.isDefined && System.currentTimeMillis() > prune_next) {
- val old_versions = global_state >>> (_.prune_history(prune_size))
+ val old_versions = global_state.change_result(_.prune_history(prune_size))
if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
prune_next = System.currentTimeMillis() + prune_delay.ms
}
@@ -460,7 +460,7 @@
msg.text match {
case Protocol.Removed(removed) =>
try {
- global_state >> (_.removed_versions(removed))
+ global_state.change(_.removed_versions(removed))
}
catch { case _: Document.State.Fail => bad_output() }
case _ => bad_output()
@@ -511,7 +511,7 @@
case Stop =>
if (phase == Session.Ready) {
_protocol_handlers = _protocol_handlers.stop(prover.get)
- global_state >> (_ => Document.State.init) // FIXME event bus!?
+ global_state.change(_ => Document.State.init) // FIXME event bus!?
phase = Session.Shutdown
prover.get.terminate
prover = None
@@ -556,7 +556,7 @@
}
case change: Session.Change
- if prover.isDefined && global_state().is_assigned(change.previous) =>
+ if prover.isDefined && global_state.value.is_assigned(change.previous) =>
handle_change(change)
case bad if !bad.isInstanceOf[Session.Change] =>
--- a/src/Pure/System/event_bus.scala Thu Apr 24 00:29:55 2014 +0200
+++ b/src/Pure/System/event_bus.scala Thu Apr 24 10:24:44 2014 +0200
@@ -17,16 +17,16 @@
private val receivers = Synchronized(List.empty[Actor])
- def += (r: Actor) { receivers >> (rs => Library.insert(r, rs)) }
+ def += (r: Actor) { receivers.change(rs => Library.insert(r, rs)) }
def += (f: Event => Unit) {
this += actor { loop { react { case x => f(x.asInstanceOf[Event]) } } }
}
- def -= (r: Actor) { receivers >> (rs => Library.remove(r, rs)) }
+ def -= (r: Actor) { receivers.change(rs => Library.remove(r, rs)) }
/* event invocation */
- def event(x: Event) { receivers().reverseIterator.foreach(_ ! x) }
+ def event(x: Event) { receivers.value.reverseIterator.foreach(_ ! x) }
}