more scalable Library.separate -- NB: JVM has tiny fixed-size stack;

--- a/src/Pure/library.scala	Tue May 14 12:46:26 2013 +0200
+++ b/src/Pure/library.scala	Tue May 14 13:46:33 2013 +0200
@@ -8,6 +8,8 @@
 package isabelle
 
 
+import scala.collection.mutable
+
 import java.util.Locale
 import java.util.concurrent.{Future => JFuture, TimeUnit}
 
@@ -32,10 +34,21 @@
   /* separated chunks */
 
   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
+  {
+    val result = new mutable.ListBuffer[A]
+    var first = true
+    for (x <- list) {
+      if (first) {
+        first = false
+        result += x
+      }
+      else {
+        result += s
+        result += x
+      }
     }
+    result.toList
+  }
 
   def separated_chunks(sep: Char, source: CharSequence): Iterator[CharSequence] =
     new Iterator[CharSequence] {