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