proper signaling after each state update (NB: ML version does this uniformly via timed_access);
authorwenzelm
Thu Apr 24 13:10:42 2014 +0200 (2014-04-24)
changeset 56694c4e77643aad6
parent 56693 0423c957b081
child 56695 963732291084
proper signaling after each state update (NB: ML version does this uniformly via timed_access);
src/Pure/Concurrent/synchronized.scala
     1.1 --- a/src/Pure/Concurrent/synchronized.scala	Thu Apr 24 12:10:26 2014 +0200
     1.2 +++ b/src/Pure/Concurrent/synchronized.scala	Thu Apr 24 13:10:42 2014 +0200
     1.3 @@ -68,10 +68,12 @@
     1.4  
     1.5    /* unconditional change */
     1.6  
     1.7 -  def change(f: A => A) = synchronized { state = f(state) }
     1.8 +  def change(f: A => A): Unit = synchronized { state = f(state); notifyAll() }
     1.9 +
    1.10    def change_result[B](f: A => (B, A)): B = synchronized {
    1.11      val (result, new_state) = f(state)
    1.12      state = new_state
    1.13 +    notifyAll()
    1.14      result
    1.15    }
    1.16  }