src/Pure/library.scala
changeset 36726 321d392ab12e
parent 36723 2b3076cfd6dd
child 36812 b8384c455b40
     1.1 --- a/src/Pure/library.scala	Thu May 06 23:07:21 2010 +0200
     1.2 +++ b/src/Pure/library.scala	Thu May 06 23:32:29 2010 +0200
     1.3 @@ -13,6 +13,15 @@
     1.4  
     1.5  object Library
     1.6  {
     1.7 +  /* separate */
     1.8 +
     1.9 +  def separate[A](s: A, list: List[A]): List[A] =
    1.10 +    list match {
    1.11 +      case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs)
    1.12 +      case _ => list
    1.13 +    }
    1.14 +
    1.15 +
    1.16    /* reverse CharSequence */
    1.17  
    1.18    class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence