# HG changeset patch
# User wenzelm
# Date 1456598873 -3600
# Node ID bccad03744074e5610db56a28576a79c59caeb51
# Parent  beb3e6c1fa5a5c52a7993c21074efd36a2a39b22
moved getopts to Scala;

diff -r beb3e6c1fa5a -r bccad0374407 lib/Tools/options
--- a/lib/Tools/options	Sat Feb 27 17:01:21 2016 +0100
+++ b/lib/Tools/options	Sat Feb 27 19:47:53 2016 +0100
@@ -4,72 +4,6 @@
 #
 # DESCRIPTION: print Isabelle system options
 
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [OPTIONS] [MORE_OPTIONS ...]"
-  echo
-  echo "  Options are:"
-  echo "    -b           include \$ISABELLE_BUILD_OPTIONS"
-  echo "    -g OPTION    get value of OPTION"
-  echo "    -l           list options"
-  echo "    -x FILE      export options to FILE in YXML format"
-  echo
-  echo "  Report Isabelle system options, augmented by MORE_OPTIONS given as"
-  echo "  arguments NAME=VAL or NAME."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-declare -a BUILD_OPTIONS=()
-GET_OPTION=""
-LIST_OPTIONS="false"
-EXPORT_FILE=""
-
-while getopts "bg:lx:" OPT
-do
-  case "$OPT" in
-    b)
-      eval "BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
-      ;;
-    g)
-      GET_OPTION="$OPTARG"
-      ;;
-    l)
-      LIST_OPTIONS="true"
-      ;;
-    x)
-      EXPORT_FILE="$OPTARG"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-[ -z "$GET_OPTION" -a "$LIST_OPTIONS" = "false" -a -z "$EXPORT_FILE" ] && usage
-
-
-## main
-
 isabelle_admin_build jars || exit $?
 
-exec "$ISABELLE_TOOL" java isabelle.Options \
-  "$GET_OPTION" "$EXPORT_FILE" "${BUILD_OPTIONS[@]}" "$@"
-
+exec "$ISABELLE_TOOL" java isabelle.Options "$@"
diff -r beb3e6c1fa5a -r bccad0374407 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Feb 27 17:01:21 2016 +0100
+++ b/src/Pure/System/options.scala	Sat Feb 27 19:47:53 2016 +0100
@@ -145,21 +145,49 @@
   def main(args: Array[String])
   {
     Command_Line.tool0 {
-      args.toList match {
-        case get_option :: export_file :: more_options =>
-          val options = (Options.init() /: more_options)(_ + _)
+      var build_options = false
+      var get_option = ""
+      var list_options = false
+      var export_file = ""
+
+      val getopts = Getopts(() => """
+Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
 
-          if (get_option != "")
-            Console.println(options.check_name(get_option).value)
+  Options are:
+    -b           include $ISABELLE_BUILD_OPTIONS
+    -g OPTION    get value of OPTION
+    -l           list options
+    -x FILE      export options to FILE in YXML format
+
+  Report Isabelle system options, augmented by MORE_OPTIONS given as
+  arguments NAME=VAL or NAME.
+""",
+        "b" -> (_ => build_options = true),
+        "g:" -> (arg => get_option = arg),
+        "l" -> (_ => list_options = true),
+        "x:" -> (arg => export_file = arg))
 
-          if (export_file != "")
-            File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
+      val more_options = getopts(args)
+      if (get_option == "" && !list_options && export_file == "") getopts.usage()
 
-          if (get_option == "" && export_file == "")
-            Console.println(options.print)
+      val options =
+      {
+        val options0 = Options.init()
+        val options1 =
+          if (build_options)
+            (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
+          else options0
+        (options1 /: more_options)(_ + _)
+      }
 
-        case _ => error("Bad arguments:\n" + cat_lines(args))
-      }
+      if (get_option != "")
+        Console.println(options.check_name(get_option).value)
+
+      if (export_file != "")
+        File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
+
+      if (get_option == "" && export_file == "")
+        Console.println(options.print)
     }
   }
 }