tuned: avoid recursion;
authorwenzelm
Sat, 18 Nov 2023 21:14:34 +0100
changeset 78990 f728be354ffb
parent 78989 d8352eb7aa7b
child 78991 ae2f5fd0bb5d
tuned: avoid recursion;
src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 18 20:51:44 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 18 21:14:34 2023 +0100
@@ -10,6 +10,7 @@
 import java.nio.file.Files
 
 import scala.annotation.tailrec
+import scala.collection.mutable
 
 
 object Isabelle_Cronjob {
@@ -154,8 +155,14 @@
   }
 
   def unknown_runs(items: List[Item]): List[List[Item]] = {
-    val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
-    if (run.nonEmpty) run :: unknown_runs(rest) else Nil
+    var rest = items
+    val result = new mutable.ListBuffer[List[Item]]
+    while (rest.nonEmpty) {
+      val (run, r) = Library.take_prefix[Item](_.unknown, rest.dropWhile(_.known))
+      if (run.nonEmpty) result += run
+      rest = r
+    }
+    result.toList
   }
 
   sealed case class Remote_Build(