1/*  Title:      Pure/System/getopts.scala
2    Author:     Makarius
3
4Support for command-line options as in GNU bash.
5*/
6
7package isabelle
8
9
10object 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
28class 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.nonEmpty =>
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.nonEmpty =>
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}
70