src/Pure/System/getopts.scala
author wenzelm
Wed, 30 Jun 2021 12:46:49 +0200
changeset 73899 4d64bc387867
parent 73359 d8a0e996614b
child 74037 c13198575f75
permissions -rw-r--r--
tuned: prefer Java interfaces;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/getopts.scala
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
     3
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
     4
Support for command-line options as in GNU bash.
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
     5
*/
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
     6
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
     7
package isabelle
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
     8
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
     9
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71383
diff changeset
    10
import scala.annotation.tailrec
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71383
diff changeset
    11
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71383
diff changeset
    12
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    13
object Getopts
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    14
{
62454
38c89353b349 tuned signature;
wenzelm
parents: 62434
diff changeset
    15
  def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts =
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    16
  {
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    17
    val options =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 71601
diff changeset
    18
      option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) {
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    19
        case (m, (s, f)) =>
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    20
          val (a, entry) =
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    21
            if (s.size == 1) (s(0), (false, f))
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    22
            else if (s.size == 2 && s.endsWith(":")) (s(0), (true, f))
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    23
            else error("Bad option specification: " + quote(s))
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    24
          if (m.isDefinedAt(a)) error("Duplicate option specification: " + quote(a.toString))
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    25
          else m + (a -> entry)
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    26
      }
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    27
    new Getopts(usage_text, options)
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    28
  }
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    29
}
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    30
62454
38c89353b349 tuned signature;
wenzelm
parents: 62434
diff changeset
    31
class Getopts private(usage_text: String, options: Map[Char, (Boolean, String => Unit)])
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    32
{
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    33
  def usage(): Nothing =
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    34
  {
67178
70576478bda9 avoid println with its extra CR on Windows;
wenzelm
parents: 62454
diff changeset
    35
    Output.writeln(usage_text, stdout = true)
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    36
    sys.exit(1)
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    37
  }
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    38
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    39
  private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    40
  private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    41
  private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1
62432
183c319b26dc tuned messages;
wenzelm
parents: 62431
diff changeset
    42
  private def print_option(opt: Char): String = quote("-" + opt.toString)
62434
4630b1748cb3 tuned messages;
wenzelm
parents: 62432
diff changeset
    43
  private def option(opt: Char, opt_arg: List[Char]): Unit =
4630b1748cb3 tuned messages;
wenzelm
parents: 62432
diff changeset
    44
    try { options(opt)._2.apply(opt_arg.mkString) }
4630b1748cb3 tuned messages;
wenzelm
parents: 62432
diff changeset
    45
    catch {
4630b1748cb3 tuned messages;
wenzelm
parents: 62432
diff changeset
    46
      case ERROR(msg) =>
4630b1748cb3 tuned messages;
wenzelm
parents: 62432
diff changeset
    47
        cat_error(msg, "The error(s) above occurred in command-line option " + print_option(opt))
4630b1748cb3 tuned messages;
wenzelm
parents: 62432
diff changeset
    48
    }
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    49
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71383
diff changeset
    50
  @tailrec private def getopts(args: List[List[Char]]): List[List[Char]] =
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    51
    args match {
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    52
      case List('-', '-') :: rest_args => rest_args
71383
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 67178
diff changeset
    53
      case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && rest_opts.nonEmpty =>
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    54
        option(opt, Nil); getopts(('-' :: rest_opts) :: rest_args)
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    55
      case List('-', opt) :: rest_args if is_option0(opt) =>
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    56
        option(opt, Nil); getopts(rest_args)
71383
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 67178
diff changeset
    57
      case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && opt_arg.nonEmpty =>
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    58
        option(opt, opt_arg); getopts(rest_args)
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    59
      case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    60
        option(opt, opt_arg); getopts(rest_args)
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    61
      case List(List('-', opt)) if is_option1(opt) =>
62432
183c319b26dc tuned messages;
wenzelm
parents: 62431
diff changeset
    62
        Output.error_message("Command-line option " + print_option(opt) + " requires an argument")
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    63
        usage()
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    64
      case ('-' :: opt :: _) :: _ if !is_option(opt) =>
62432
183c319b26dc tuned messages;
wenzelm
parents: 62431
diff changeset
    65
        if (opt != '?') Output.error_message("Illegal command-line option " + print_option(opt))
62431
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    66
        usage()
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    67
      case _ => args
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    68
  }
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    69
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    70
  def apply(args: List[String]): List[String] = getopts(args.map(_.toList)).map(_.mkString)
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    71
  def apply(args: Array[String]): List[String] = apply(args.toList)
fbccea37091d support for command-line options as in GNU bash;
wenzelm
parents:
diff changeset
    72
}