more uniform synchronized variables;
authorwenzelm
Thu Apr 24 00:27:06 2014 +0200 (2014-04-24)
changeset 56685535d59d4ed12
parent 56677 660ffb526069
child 56686 2386d1a3ca8f
more uniform synchronized variables;
src/Pure/Concurrent/counter.scala
src/Pure/Concurrent/synchronized.ML
src/Pure/Concurrent/synchronized.scala
src/Pure/Concurrent/volatile.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Concurrent/counter.scala	Wed Apr 23 17:57:56 2014 +0200
     1.2 +++ b/src/Pure/Concurrent/counter.scala	Thu Apr 24 00:27:06 2014 +0200
     1.3 @@ -25,5 +25,7 @@
     1.4      count -= 1
     1.5      count
     1.6    }
     1.7 +
     1.8 +  override def toString: String = count.toString
     1.9  }
    1.10  
     2.1 --- a/src/Pure/Concurrent/synchronized.ML	Wed Apr 23 17:57:56 2014 +0200
     2.2 +++ b/src/Pure/Concurrent/synchronized.ML	Thu Apr 24 00:27:06 2014 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      Pure/Concurrent/synchronized.ML
     2.5      Author:     Fabian Immler and Makarius
     2.6  
     2.7 -State variables with synchronized access.
     2.8 +Synchronized variables.
     2.9  *)
    2.10  
    2.11  signature SYNCHRONIZED =
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Concurrent/synchronized.scala	Thu Apr 24 00:27:06 2014 +0200
     3.3 @@ -0,0 +1,29 @@
     3.4 +/*  Title:      Pure/Concurrent/synchronized.scala
     3.5 +    Module:     PIDE
     3.6 +    Author:     Makarius
     3.7 +
     3.8 +Synchronized variables.
     3.9 +*/
    3.10 +
    3.11 +package isabelle
    3.12 +
    3.13 +
    3.14 +object Synchronized
    3.15 +{
    3.16 +  def apply[A](init: A): Synchronized[A] = new Synchronized(init)
    3.17 +}
    3.18 +
    3.19 +
    3.20 +final class Synchronized[A] private(init: A)
    3.21 +{
    3.22 +  private var state: A = init
    3.23 +  def apply(): A = synchronized { state }
    3.24 +  def >> (f: A => A) = synchronized { state = f(state) }
    3.25 +  def >>>[B] (f: A => (B, A)): B = synchronized {
    3.26 +    val (result, new_state) = f(state)
    3.27 +    state = new_state
    3.28 +    result
    3.29 +  }
    3.30 +
    3.31 +  override def toString: String = state.toString
    3.32 +}
     4.1 --- a/src/Pure/Concurrent/volatile.scala	Wed Apr 23 17:57:56 2014 +0200
     4.2 +++ b/src/Pure/Concurrent/volatile.scala	Thu Apr 24 00:27:06 2014 +0200
     4.3 @@ -25,5 +25,7 @@
     4.4      state = new_state
     4.5      result
     4.6    }
     4.7 +
     4.8 +  override def toString: String = state.toString
     4.9  }
    4.10  
     5.1 --- a/src/Pure/build-jars	Wed Apr 23 17:57:56 2014 +0200
     5.2 +++ b/src/Pure/build-jars	Thu Apr 24 00:27:06 2014 +0200
     5.3 @@ -12,6 +12,7 @@
     5.4    Concurrent/counter.scala
     5.5    Concurrent/future.scala
     5.6    Concurrent/simple_thread.scala
     5.7 +  Concurrent/synchronized.scala
     5.8    Concurrent/volatile.scala
     5.9    General/antiquote.scala
    5.10    General/bytes.scala