# HG changeset patch
# User wenzelm
# Date 1368531993 -7200
# Node ID a8ffd3692f57e4693ef854e11e08a602e3e8cf0b
# Parent  fe16d1128a14857b47f355487a59328efe65746b
more scalable Library.separate -- NB: JVM has tiny fixed-size stack;

diff -r fe16d1128a14 -r a8ffd3692f57 src/Pure/library.scala
--- 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] {