minor performance tuning: prefer mutable.ListBuffer;
authorwenzelm
Fri, 31 Oct 2025 18:21:34 +0100
changeset 83433 e26f102d2498
parent 83432 6b2db426f1b3
child 83434 5c70d1c27a2e
minor performance tuning: prefer mutable.ListBuffer;
src/Tools/VSCode/src/language_server.scala
src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/language_server.scala	Fri Oct 31 11:31:36 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Fri Oct 31 18:21:34 2025 +0100
@@ -14,6 +14,8 @@
 import isabelle._
 
 import java.io.{PrintStream, OutputStream, File => JFile}
+
+import scala.collection.mutable
 import scala.annotation.tailrec
 
 
@@ -32,8 +34,8 @@
           var logic_ancestor: Option[String] = None
           var log_file: Option[Path] = None
           var logic_requirements = false
-          var dirs: List[Path] = Nil
-          var include_sessions: List[String] = Nil
+          val dirs = new mutable.ListBuffer[Path]
+          val include_sessions = new mutable.ListBuffer[String]
           var logic = default_logic
           var modes: List[String] = Nil
           var no_build = false
@@ -60,8 +62,8 @@
             "A:" -> (arg => logic_ancestor = Some(arg)),
             "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
             "R:" -> (arg => { logic = arg; logic_requirements = true }),
-            "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
-            "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
+            "d:" -> (arg => dirs += Path.explode(File.standard_path(arg))),
+            "i:" -> (arg => include_sessions += arg),
             "l:" -> (arg => logic = arg),
             "m:" -> (arg => modes = arg :: modes),
             "n" -> (_ => no_build = true),
@@ -74,8 +76,8 @@
           val log = Logger.make_file(log_file)
           val channel = new Channel(System.in, System.out, log, verbose)
           val server =
-            new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
-              include_sessions = include_sessions, session_ancestor = logic_ancestor,
+            new Language_Server(channel, options, session_name = logic, session_dirs = dirs.toList,
+              include_sessions = include_sessions.toList, session_ancestor = logic_ancestor,
               session_requirements = logic_requirements, session_no_build = no_build,
               modes = modes, log = log)
 
--- a/src/Tools/VSCode/src/vscode_main.scala	Fri Oct 31 11:31:36 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala	Fri Oct 31 18:21:34 2025 +0100
@@ -11,6 +11,8 @@
 
 import java.util.zip.ZipFile
 
+import scala.collection.mutable
+
 
 object VSCode_Main {
   /* vscodium command-line interface */
@@ -179,16 +181,14 @@
         var logic_requirements = false
         var uninstall = false
         var vsix_path = default_vsix_path
-        var session_dirs = List.empty[Path]
-        var include_sessions = List.empty[String]
+        val session_dirs = new mutable.ListBuffer[Path]
+        val include_sessions = new mutable.ListBuffer[String]
         var logic = ""
-        var modes = List.empty[String]
+        val modes = new mutable.ListBuffer[String]
         var no_build = false
-        var options = List.empty[String]
+        val options = new mutable.ListBuffer[String]
         var verbose = false
 
-        def add_option(opt: String): Unit = options = options ::: List(opt)
-
         val getopts = Getopts("""
 Usage: isabelle vscode [OPTIONS] [ARGUMENTS] [-- VSCODE_OPTIONS]
 
@@ -224,15 +224,15 @@
           "R:" -> (arg => { logic = arg; logic_requirements = true }),
           "U" -> (_ => uninstall = true),
           "V:" -> (arg => vsix_path = Path.explode(arg)),
-          "d:" -> (arg => session_dirs = session_dirs ::: List(Path.explode(arg))),
-          "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
+          "d:" -> (arg => session_dirs += Path.explode(arg)),
+          "i:" -> (arg => include_sessions += arg),
           "l:" -> (arg => { logic = arg; logic_requirements = false }),
-          "m:" -> (arg => modes = modes ::: List(arg)),
+          "m:" -> (arg => modes += arg),
           "n" -> (_ => no_build = true),
-          "o:" -> add_option,
-          "p:" -> (arg => add_option("process_policy=" + arg)),
-          "s" -> (_ => add_option("system_heaps=true")),
-          "u" -> (_ => add_option("system_heaps=false")),
+          "o:" -> (arg => options += arg),
+          "p:" -> (arg => options += ("process_policy=" + arg)),
+          "s" -> (_ => options += "system_heaps=true"),
+          "u" -> (_ => options += "system_heaps=false"),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
@@ -249,9 +249,9 @@
 
         run_vscodium(
           more_args ::: (if (edit_extension) List(File.platform_path(extension_dir)) else Nil),
-          options = options, logic = logic, logic_ancestor = logic_ancestor,
-          logic_requirements = logic_requirements, session_dirs = session_dirs,
-          include_sessions = include_sessions, modes = modes, no_build = no_build,
+          options = options.toList, logic = logic, logic_ancestor = logic_ancestor,
+          logic_requirements = logic_requirements, session_dirs = session_dirs.toList,
+          include_sessions = include_sessions.toList, modes = modes.toList, no_build = no_build,
           server_log = server_log, verbose = verbose, background = background,
           progress = app_progress).check
       })