minor performance tuning;
authorwenzelm
Sun, 09 Nov 2025 13:11:56 +0100
changeset 83538 be77b8f48b7b
parent 83537 7f14cf99db0d
child 83539 089dc60aadce
minor performance tuning;
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_history.scala	Sun Nov 09 13:02:13 2025 +0100
+++ b/src/Pure/Admin/build_history.scala	Sun Nov 09 13:11:56 2025 +0100
@@ -6,6 +6,8 @@
 
 package isabelle
 
+import scala.collection.mutable
+
 
 object Build_History {
   /* log files */
@@ -404,14 +406,14 @@
       var component_repository = Components.static_component_repository
       var components_base = Components.dynamic_components_base
       var arch_apple = false
-      var more_settings: List[String] = Nil
-      var more_preferences: List[String] = Nil
+      val more_settings = new mutable.ListBuffer[String]
+      val more_preferences = new mutable.ListBuffer[String]
       var fresh = false
       var hostname = ""
       var arch_64 = false
       var output_file = ""
       var ml_statistics_step = 1
-      var build_tags = List.empty[String]
+      val build_tags = new mutable.ListBuffer[String]
       var verbose = false
       var exit_code = false
 
@@ -464,7 +466,7 @@
         "S:" -> (arg => components_base = arg),
         "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
         "a" -> (_ => arch_apple = true),
-        "e:" -> (arg => more_settings = more_settings ::: List(arg)),
+        "e:" -> (arg => more_settings += arg),
         "f" -> (_ => fresh = true),
         "h:" -> (arg => hostname = arg),
         "m:" ->
@@ -474,9 +476,9 @@
             case bad => error("Bad processor architecture: " + quote(bad))
           },
         "o:" -> (arg => output_file = arg),
-        "p:" -> (arg => more_preferences = more_preferences ::: List(arg)),
+        "p:" -> (arg => more_preferences += arg),
         "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
-        "t:" -> (arg => build_tags = build_tags ::: List(arg)),
+        "t:" -> (arg => build_tags += arg),
         "v" -> (_ => verbose = true),
         "x" -> (_ => exit_code = true))
 
@@ -497,9 +499,9 @@
           fresh = fresh, hostname = hostname, multicore_base = multicore_base,
           multicore_list = multicore_list, arch_64 = arch_64, arch_apple = arch_apple,
           heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
-          max_heap = max_heap, more_settings = more_settings,
-          more_preferences = more_preferences, verbose = verbose, build_tags = build_tags,
-          build_args = build_args)
+          max_heap = max_heap, more_settings = more_settings.toList,
+          more_preferences = more_preferences.toList, verbose = verbose,
+          build_tags = build_tags.toList, build_args = build_args)
 
       if (output_file.isEmpty) {
         for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true)
--- a/src/Pure/Admin/build_release.scala	Sun Nov 09 13:02:13 2025 +0100
+++ b/src/Pure/Admin/build_release.scala	Sun Nov 09 13:11:56 2025 +0100
@@ -8,6 +8,8 @@
 
 import isabelle.find_facts.Find_Facts
 
+import scala.collection.mutable
+
 
 object Build_Release {
   /** release context **/
@@ -893,7 +895,7 @@
       var source_archive = ""
       var website: Option[Path] = None
       var build_sessions: List[String] = Nil
-      var more_components: List[Path] = Nil
+      val more_components = new mutable.ListBuffer[Path]
       var parallel_jobs = 1
       var build_library = false
       var options = Options.init()
@@ -933,7 +935,7 @@
           {
             val path = Path.explode(arg)
             Components.Archive.get_name(path.file_name)
-            more_components = more_components ::: List(path)
+            more_components += path
           }),
         "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
         "l" -> (_ => build_library = true),
@@ -967,7 +969,7 @@
         }
 
       build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
-        more_components = more_components, build_sessions = build_sessions,
+        more_components = more_components.toList, build_sessions = build_sessions,
         parallel_jobs = parallel_jobs, website = website)
     }
   }