# HG changeset patch
# User wenzelm
# Date 1456588350 -3600
# Node ID 2c390ad93bc8750e5ed970e9597d17805aca40e1
# Parent  4630b1748cb3362a8170959e86a89ee40e521b99
moved getopts to Scala;

diff -r 4630b1748cb3 -r 2c390ad93bc8 Admin/lib/Tools/build_doc
--- a/Admin/lib/Tools/build_doc	Sat Feb 27 16:51:36 2016 +0100
+++ b/Admin/lib/Tools/build_doc	Sat Feb 27 16:52:30 2016 +0100
@@ -4,7 +4,8 @@
 #
 # DESCRIPTION: build Isabelle documentation
 
-## settings
+isabelle_admin_build jars || exit $?
+
 
 case "$ISABELLE_JAVA_PLATFORM" in
   x86-*)
@@ -15,75 +16,6 @@
     ;;
 esac
 
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [OPTIONS] [DOCS ...]"
-  echo
-  echo "  Options are:"
-  echo "    -a           select all documentation sessions"
-  echo "    -j INT       maximum number of parallel jobs (default 1)"
-  echo "    -s           system build mode"
-  echo
-  echo "  Build Isabelle documentation from documentation sessions with"
-  echo "  suitable document_variants entry."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-function check_number()
-{
-  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
-}
-
-
-## process command line
-
-ALL_DOCS="false"
-MAX_JOBS="1"
-SYSTEM_MODE="false"
-
-while getopts "aj:s" OPT
-do
-  case "$OPT" in
-    a)
-      ALL_DOCS="true"
-      ;;
-    j)
-      check_number "$OPTARG"
-      MAX_JOBS="$OPTARG"
-      ;;
-    s)
-      SYSTEM_MODE="true"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-[ "$ALL_DOCS" = false -a "$#" -eq 0 ] && usage
-
-
-## main
-
-isabelle_admin_build jars || exit $?
-
 declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
 
-"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc \
-  "$ALL_DOCS" "$MAX_JOBS" "$SYSTEM_MODE" "$@"
-
+"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc "$@"
diff -r 4630b1748cb3 -r 2c390ad93bc8 src/Pure/Tools/build_doc.scala
--- a/src/Pure/Tools/build_doc.scala	Sat Feb 27 16:51:36 2016 +0100
+++ b/src/Pure/Tools/build_doc.scala	Sat Feb 27 16:52:30 2016 +0100
@@ -72,20 +72,35 @@
   def main(args: Array[String])
   {
     Command_Line.tool {
-      args.toList match {
-        case
-          Properties.Value.Boolean(all_docs) ::
-          Properties.Value.Int(max_jobs) ::
-          Properties.Value.Boolean(system_mode) ::
-          Command_Line.Chunks(docs) =>
-            val options = Options.init()
-            val progress = new Console_Progress()
-            progress.interrupt_handler {
-              build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
-            }
-        case _ => error("Bad arguments:\n" + cat_lines(args))
+      var all_docs = false
+      var max_jobs = 1
+      var system_mode = false
+
+      val getopts =
+        Getopts(() => """
+Usage: isabelle build_doc [OPTIONS] [DOCS ...]"
+
+  Options are:
+    -a           select all documentation sessions
+    -j INT       maximum number of parallel jobs (default 1)
+    -s           system build mode
+
+  Build Isabelle documentation from documentation sessions with
+  suitable document_variants entry.
+""",
+        "a" -> (_ => all_docs = true),
+        "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
+        "s" -> (_ => system_mode = true))
+
+      val docs = getopts(args)
+
+      if (!all_docs && docs.isEmpty) getopts.usage()
+
+      val options = Options.init()
+      val progress = new Console_Progress()
+      progress.interrupt_handler {
+        build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
       }
     }
   }
 }
-