src/Pure/System/getopts.scala

--- a/src/Pure/System/getopts.scala	Thu Nov 06 10:55:39 2025 +0000
+++ b/src/Pure/System/getopts.scala	Fri Nov 07 16:43:04 2025 +0100
@@ -27,9 +27,12 @@
 }
 
 class Getopts private(usage_text: => String, options: Map[Char, (Boolean, String => Unit)]) {
-  def usage(): Nothing = {
-    Output.writeln(usage_text, stdout = true)
-    sys.exit(Process_Result.RC.error)
+  def usage(internal: Boolean = false): Nothing = {
+    if (internal) error(usage_text)
+    else {
+      Output.writeln(usage_text, stdout = true)
+      sys.exit(Process_Result.RC.error)
+    }
   }
 
   private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)
@@ -43,26 +46,30 @@
         cat_error(msg, "The error(s) above occurred in command-line option " + print_option(opt))
     }
 
-  @tailrec private def getopts(args: List[List[Char]]): List[List[Char]] =
+  private def err(msg: String, internal: Boolean): Nothing =
+    if (internal) cat_error(msg, usage_text)
+    else { Output.error_message(msg); usage() }
+
+  @tailrec private def getopts(args: List[List[Char]], internal: Boolean): List[List[Char]] =
     args match {
       case List('-', '-') :: rest_args => rest_args
       case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && rest_opts.nonEmpty =>
-        option(opt, Nil); getopts(('-' :: rest_opts) :: rest_args)
+        option(opt, Nil); getopts(('-' :: rest_opts) :: rest_args, internal)
       case List('-', opt) :: rest_args if is_option0(opt) =>
-        option(opt, Nil); getopts(rest_args)
+        option(opt, Nil); getopts(rest_args, internal)
       case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && opt_arg.nonEmpty =>
-        option(opt, opt_arg); getopts(rest_args)
+        option(opt, opt_arg); getopts(rest_args, internal)
       case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
-        option(opt, opt_arg); getopts(rest_args)
+        option(opt, opt_arg); getopts(rest_args, internal)
       case List(List('-', opt)) if is_option1(opt) =>
-        Output.error_message("Command-line option " + print_option(opt) + " requires an argument")
-        usage()
+        err("Command-line option " + print_option(opt) + " requires an argument", internal)
       case ('-' :: opt :: _) :: _ if !is_option(opt) =>
-        if (opt != '?') Output.error_message("Illegal command-line option " + print_option(opt))
-        usage()
+        err(if (opt != '?') "Illegal command-line option " + print_option(opt) else "", internal)
       case _ => args
   }
 
-  def apply(args: List[String]): List[String] = getopts(args.map(_.toList)).map(_.mkString)
+  def apply(args: List[String], internal: Boolean): List[String] =
+    getopts(args.map(_.toList), internal).map(_.mkString)
+  def apply(args: List[String]): List[String] = apply(args, false)
   def apply(args: Array[String]): List[String] = apply(args.toList)
 }