more canonical list operations;
authorwenzelm
Thu Apr 24 10:30:55 2014 +0200 (2014-04-24)
changeset 56688f3932166a33d
parent 56687 7fb98325722a
child 56689 b8b8b4ff8ad5
more canonical list operations;
src/Pure/System/event_bus.scala
src/Pure/library.scala
     1.1 --- a/src/Pure/System/event_bus.scala	Thu Apr 24 10:24:44 2014 +0200
     1.2 +++ b/src/Pure/System/event_bus.scala	Thu Apr 24 10:30:55 2014 +0200
     1.3 @@ -17,13 +17,13 @@
     1.4  
     1.5    private val receivers = Synchronized(List.empty[Actor])
     1.6  
     1.7 -  def += (r: Actor) { receivers.change(rs => Library.insert(r, rs)) }
     1.8 +  def += (r: Actor) { receivers.change(Library.insert(r)) }
     1.9  
    1.10    def += (f: Event => Unit) {
    1.11      this += actor { loop { react { case x => f(x.asInstanceOf[Event]) } } }
    1.12    }
    1.13  
    1.14 -  def -= (r: Actor) { receivers.change(rs => Library.remove(r, rs)) }
    1.15 +  def -= (r: Actor) { receivers.change(Library.remove(r)) }
    1.16  
    1.17  
    1.18    /* event invocation */
     2.1 --- a/src/Pure/library.scala	Thu Apr 24 10:24:44 2014 +0200
     2.2 +++ b/src/Pure/library.scala	Thu Apr 24 10:30:55 2014 +0200
     2.3 @@ -155,10 +155,10 @@
     2.4  
     2.5    /* canonical list operations */
     2.6  
     2.7 -  def member[A, B](x: B, xs: List[A]): Boolean = xs.exists(_ == x)
     2.8 -  def insert[A](x: A, xs: List[A]): List[A] = if (member(x, xs)) xs else x :: xs
     2.9 -  def remove[A, B](x: B, xs: List[A]): List[A] = if (member(x, xs)) xs.filterNot(_ == x) else xs
    2.10 -  def update[A](x: A, xs: List[A]): List[A] = x :: remove(x, xs)
    2.11 +  def member[A, B](xs: List[A])(x: B): Boolean = xs.exists(_ == x)
    2.12 +  def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
    2.13 +  def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
    2.14 +  def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
    2.15  
    2.16  
    2.17    /* Java futures */