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