src/Pure/System/getopts.scala

tuned --- based on hints by IntelliJ IDEA;

/*  Title:      Pure/System/getopts.scala
    Author:     Makarius

Support for command-line options as in GNU bash.
*/

package isabelle


import scala.annotation.tailrec


object Getopts
{
  def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts =
  {
    val options =
      option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) {
        case (m, (s, f)) =>
          val (a, entry) =
            if (s.length == 1) (s(0), (false, f))
            else if (s.length == 2 && s.endsWith(":")) (s(0), (true, f))
            else error("Bad option specification: " + quote(s))
          if (m.isDefinedAt(a)) error("Duplicate option specification: " + quote(a.toString))
          else m + (a -> entry)
      }
    new Getopts(usage_text, options)
  }
}

class Getopts private(usage_text: String, options: Map[Char, (Boolean, String => Unit)])
{
  def usage(): Nothing =
  {
    Output.writeln(usage_text, stdout = true)
    sys.exit(1)
  }

  private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)
  private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1
  private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1
  private def print_option(opt: Char): String = quote("-" + opt.toString)
  private def option(opt: Char, opt_arg: List[Char]): Unit =
    try { options(opt)._2.apply(opt_arg.mkString) }
    catch {
      case ERROR(msg) =>
        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]] =
    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)
      case List('-', opt) :: rest_args if is_option0(opt) =>
        option(opt, Nil); getopts(rest_args)
      case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && opt_arg.nonEmpty =>
        option(opt, opt_arg); getopts(rest_args)
      case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
        option(opt, opt_arg); getopts(rest_args)
      case List(List('-', opt)) if is_option1(opt) =>
        Output.error_message("Command-line option " + print_option(opt) + " requires an argument")
        usage()
      case ('-' :: opt :: _) :: _ if !is_option(opt) =>
        if (opt != '?') Output.error_message("Illegal command-line option " + print_option(opt))
        usage()
      case _ => args
  }

  def apply(args: List[String]): List[String] = getopts(args.map(_.toList)).map(_.mkString)
  def apply(args: Array[String]): List[String] = apply(args.toList)
}