minor performance tuning;

--- a/src/Pure/ML/ml_console.scala	Sat Nov 08 20:50:41 2025 +0100
+++ b/src/Pure/ML/ml_console.scala	Sun Nov 09 13:01:30 2025 +0100
@@ -7,13 +7,16 @@
 package isabelle
 
 
+import scala.collection.mutable
+
+
 object ML_Console {
   /* command line entry point */
 
   def main(args: Array[String]): Unit = {
     Command_Line.tool {
-      var dirs: List[Path] = Nil
-      var include_sessions: List[String] = Nil
+      val dir_args = new mutable.ListBuffer[Path]
+      val include_sessions = new mutable.ListBuffer[String]
       var logic = Isabelle_System.default_logic()
       var modes: List[String] = Nil
       var no_build = false
@@ -36,8 +39,8 @@
   in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
   quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
 """,
-        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
-        "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
+        "d:" -> (arg => dir_args += Path.explode(arg)),
+        "i:" -> (arg => include_sessions += arg),
         "l:" -> (arg => logic = arg),
         "m:" -> (arg => modes = arg :: modes),
         "n" -> (_ => no_build = true),
@@ -47,6 +50,7 @@
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
+      val dirs = dir_args.toList
 
       val store = Store(options)
 
@@ -68,7 +72,7 @@
         }
         else {
           Sessions.background(
-            options, logic, dirs = dirs, include_sessions = include_sessions).check_errors
+            options, logic, dirs = dirs, include_sessions = include_sessions.toList).check_errors
         }
 
       val session_heaps =

--- a/src/Pure/ML/ml_process.scala	Sat Nov 08 20:50:41 2025 +0100
+++ b/src/Pure/ML/ml_process.scala	Sun Nov 09 13:01:30 2025 +0100
@@ -9,6 +9,8 @@
 
 import java.util.{Map => JMap, HashMap}
 
+import scala.collection.mutable
+
 
 object ML_Process {
   /* process */
@@ -132,8 +134,8 @@
 
   def tool_body(args: List[String], internal: Boolean = false): Process_Result = {
     var cwd = Path.current
-    var dirs: List[Path] = Nil
-    var eval_args: List[String] = Nil
+    val dirs = new mutable.ListBuffer[Path]
+    val eval_args = new mutable.ListBuffer[String]
     var logic = Isabelle_System.default_logic()
     var modes: List[String] = Nil
     var options = Options.init()
@@ -155,9 +157,9 @@
   Run the raw ML process without Isabelle/Scala context.
 """,
       "C:" -> (arg => cwd = Path.explode(arg)),
-      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
-      "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
-      "f:" -> (arg => eval_args = eval_args ::: List("--use", File.platform_path(arg))),
+      "d:" -> (arg => dirs += Path.explode(arg)),
+      "e:" -> (arg => eval_args ++= List("--eval", arg)),
+      "f:" -> (arg => eval_args ++= List("--use", File.platform_path(arg))),
       "l:" -> (arg => logic = arg),
       "m:" -> (arg => modes = arg :: modes),
       "o:" -> (arg => options = options + arg),
@@ -167,12 +169,12 @@
     if (more_args.nonEmpty) getopts.usage(internal = internal)
 
     val store = Store(options)
-    val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
+    val session_background = Sessions.background(options, logic, dirs = dirs.toList).check_errors
     val session_heaps = store.session_heaps(session_background, logic = logic)
 
     val process =
       ML_Process(options, session_background, session_heaps,
-        args = eval_args, modes = modes, cwd = cwd, redirect = redirect)
+        args = eval_args.toList, modes = modes, cwd = cwd, redirect = redirect)
     if (internal) process.result()
     else {
       process.result(