# HG changeset patch
# User wenzelm
# Date 1273181549 -7200
# Node ID 321d392ab12e0a798143ff0f9b318ca962751dbf
# Parent  58020b59baf7f262a8ea90a2b2c3be954f476f79
added separate;

diff -r 58020b59baf7 -r 321d392ab12e src/Pure/library.scala
--- a/src/Pure/library.scala	Thu May 06 23:07:21 2010 +0200
+++ b/src/Pure/library.scala	Thu May 06 23:32:29 2010 +0200
@@ -13,6 +13,15 @@
 
 object Library
 {
+  /* separate */
+
+  def separate[A](s: A, list: List[A]): List[A] =
+    list match {
+      case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs)
+      case _ => list
+    }
+
+
   /* reverse CharSequence */
 
   class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence