src/Pure/library.scala
changeset 67434 a38c74b0886d
parent 67431 84e143e64336
child 67436 e446505a4ec6
equal deleted inserted replaced
67433:e0c0c1f0e3e7 67434:a38c74b0886d
   221   /* lists */
   221   /* lists */
   222 
   222 
   223   def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
   223   def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
   224     (xs.takeWhile(pred), xs.dropWhile(pred))
   224     (xs.takeWhile(pred), xs.dropWhile(pred))
   225 
   225 
       
   226   def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
       
   227   {
       
   228     val rev_xs = xs.reverse
       
   229     (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse)
       
   230   }
       
   231 
       
   232   def trim[A](pred: A => Boolean, xs: List[A]): List[A] =
       
   233     take_suffix(pred, take_prefix(pred, xs)._2)._1
       
   234 
   226   def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   235   def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   227   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   236   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   228   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   237   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   229   def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
   238   def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
   230 
   239