src/Pure/System/getopts.scala
author wenzelm
Sun Dec 10 20:29:00 2017 +0100 (18 months ago)
changeset 67178 70576478bda9
parent 62454 38c89353b349
permissions -rw-r--r--
avoid println with its extra CR on Windows;
wenzelm@62431
     1
/*  Title:      Pure/System/getopts.scala
wenzelm@62431
     2
    Author:     Makarius
wenzelm@62431
     3
wenzelm@62431
     4
Support for command-line options as in GNU bash.
wenzelm@62431
     5
*/
wenzelm@62431
     6
wenzelm@62431
     7
package isabelle
wenzelm@62431
     8
wenzelm@62431
     9
wenzelm@62431
    10
object Getopts
wenzelm@62431
    11
{
wenzelm@62454
    12
  def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts =
wenzelm@62431
    13
  {
wenzelm@62431
    14
    val options =
wenzelm@62431
    15
      (Map.empty[Char, (Boolean, String => Unit)] /: option_specs) {
wenzelm@62431
    16
        case (m, (s, f)) =>
wenzelm@62431
    17
          val (a, entry) =
wenzelm@62431
    18
            if (s.size == 1) (s(0), (false, f))
wenzelm@62431
    19
            else if (s.size == 2 && s.endsWith(":")) (s(0), (true, f))
wenzelm@62431
    20
            else error("Bad option specification: " + quote(s))
wenzelm@62431
    21
          if (m.isDefinedAt(a)) error("Duplicate option specification: " + quote(a.toString))
wenzelm@62431
    22
          else m + (a -> entry)
wenzelm@62431
    23
      }
wenzelm@62431
    24
    new Getopts(usage_text, options)
wenzelm@62431
    25
  }
wenzelm@62431
    26
}
wenzelm@62431
    27
wenzelm@62454
    28
class Getopts private(usage_text: String, options: Map[Char, (Boolean, String => Unit)])
wenzelm@62431
    29
{
wenzelm@62431
    30
  def usage(): Nothing =
wenzelm@62431
    31
  {
wenzelm@67178
    32
    Output.writeln(usage_text, stdout = true)
wenzelm@62431
    33
    sys.exit(1)
wenzelm@62431
    34
  }
wenzelm@62431
    35
wenzelm@62431
    36
  private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)
wenzelm@62431
    37
  private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1
wenzelm@62431
    38
  private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1
wenzelm@62432
    39
  private def print_option(opt: Char): String = quote("-" + opt.toString)
wenzelm@62434
    40
  private def option(opt: Char, opt_arg: List[Char]): Unit =
wenzelm@62434
    41
    try { options(opt)._2.apply(opt_arg.mkString) }
wenzelm@62434
    42
    catch {
wenzelm@62434
    43
      case ERROR(msg) =>
wenzelm@62434
    44
        cat_error(msg, "The error(s) above occurred in command-line option " + print_option(opt))
wenzelm@62434
    45
    }
wenzelm@62431
    46
wenzelm@62431
    47
  private def getopts(args: List[List[Char]]): List[List[Char]] =
wenzelm@62431
    48
    args match {
wenzelm@62431
    49
      case List('-', '-') :: rest_args => rest_args
wenzelm@62431
    50
      case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && !rest_opts.isEmpty =>
wenzelm@62431
    51
        option(opt, Nil); getopts(('-' :: rest_opts) :: rest_args)
wenzelm@62431
    52
      case List('-', opt) :: rest_args if is_option0(opt) =>
wenzelm@62431
    53
        option(opt, Nil); getopts(rest_args)
wenzelm@62431
    54
      case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && !opt_arg.isEmpty =>
wenzelm@62431
    55
        option(opt, opt_arg); getopts(rest_args)
wenzelm@62431
    56
      case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
wenzelm@62431
    57
        option(opt, opt_arg); getopts(rest_args)
wenzelm@62431
    58
      case List(List('-', opt)) if is_option1(opt) =>
wenzelm@62432
    59
        Output.error_message("Command-line option " + print_option(opt) + " requires an argument")
wenzelm@62431
    60
        usage()
wenzelm@62431
    61
      case ('-' :: opt :: _) :: _ if !is_option(opt) =>
wenzelm@62432
    62
        if (opt != '?') Output.error_message("Illegal command-line option " + print_option(opt))
wenzelm@62431
    63
        usage()
wenzelm@62431
    64
      case _ => args
wenzelm@62431
    65
  }
wenzelm@62431
    66
wenzelm@62431
    67
  def apply(args: List[String]): List[String] = getopts(args.map(_.toList)).map(_.mkString)
wenzelm@62431
    68
  def apply(args: Array[String]): List[String] = apply(args.toList)
wenzelm@62431
    69
}