# HG changeset patch
# User wenzelm
# Date 1456586342 -3600
# Node ID fbccea37091d9b2e31c0b1c49d6c31a0443e692b
# Parent  9527ff088c15799d5a7604fa974242f8b75b87a8
support for command-line options as in GNU bash;

diff -r 9527ff088c15 -r fbccea37091d src/Pure/System/getopts.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/getopts.scala	Sat Feb 27 16:19:02 2016 +0100
@@ -0,0 +1,63 @@
+/*  Title:      Pure/System/getopts.scala
+    Author:     Makarius
+
+Support for command-line options as in GNU bash.
+*/
+
+package isabelle
+
+
+object Getopts
+{
+  def apply(usage_text: () => String, option_specs: (String, String => Unit)*): Getopts =
+  {
+    val options =
+      (Map.empty[Char, (Boolean, String => Unit)] /: option_specs) {
+        case (m, (s, f)) =>
+          val (a, entry) =
+            if (s.size == 1) (s(0), (false, f))
+            else if (s.size == 2 && s.endsWith(":")) (s(0), (true, f))
+            else error("Bad option specification: " + quote(s))
+          if (m.isDefinedAt(a)) error("Duplicate option specification: " + quote(a.toString))
+          else m + (a -> entry)
+      }
+    new Getopts(usage_text, options)
+  }
+}
+
+class Getopts private(usage_text: () => String, options: Map[Char, (Boolean, String => Unit)])
+{
+  def usage(): Nothing =
+  {
+    Console.println(usage_text())
+    sys.exit(1)
+  }
+
+  private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)
+  private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1
+  private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1
+  private def option(opt: Char, opt_arg: List[Char]): Unit = options(opt)._2.apply(opt_arg.mkString)
+
+  private def getopts(args: List[List[Char]]): List[List[Char]] =
+    args match {
+      case List('-', '-') :: rest_args => rest_args
+      case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && !rest_opts.isEmpty =>
+        option(opt, Nil); getopts(('-' :: rest_opts) :: rest_args)
+      case List('-', opt) :: rest_args if is_option0(opt) =>
+        option(opt, Nil); getopts(rest_args)
+      case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && !opt_arg.isEmpty =>
+        option(opt, opt_arg); getopts(rest_args)
+      case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
+        option(opt, opt_arg); getopts(rest_args)
+      case List(List('-', opt)) if is_option1(opt) =>
+        Output.error_message("Command-line option " + quote(opt.toString) + " requires an argument")
+        usage()
+      case ('-' :: opt :: _) :: _ if !is_option(opt) =>
+        Output.error_message("Illegal command-line option " + quote(opt.toString))
+        usage()
+      case _ => args
+  }
+
+  def apply(args: List[String]): List[String] = getopts(args.map(_.toList)).map(_.mkString)
+  def apply(args: Array[String]): List[String] = apply(args.toList)
+}
diff -r 9527ff088c15 -r fbccea37091d src/Pure/build-jars
--- a/src/Pure/build-jars	Fri Feb 26 22:44:11 2016 +0100
+++ b/src/Pure/build-jars	Sat Feb 27 16:19:02 2016 +0100
@@ -75,6 +75,7 @@
   ROOT.scala
   System/command_line.scala
   System/cygwin.scala
+  System/getopts.scala
   System/invoke_scala.scala
   System/isabelle_charset.scala
   System/isabelle_process.scala