moved getopts to Scala;

--- a/lib/Tools/doc	Sat Feb 27 19:47:53 2016 +0100
+++ b/lib/Tools/doc	Sat Feb 27 19:57:36 2016 +0100
@@ -4,34 +4,6 @@
 #
 # DESCRIPTION: view Isabelle documentation
 
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [DOC ...]"
-  echo
-  echo "  View Isabelle documentation."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## args
-
-[ "$#" -eq 1 -a "$1" = "-?" ] && usage
-
-
-## main
-
 isabelle_admin_build jars || exit $?
 
 "$ISABELLE_TOOL" java isabelle.Doc "$@"
-

--- a/src/Pure/Tools/doc.scala	Sat Feb 27 19:47:53 2016 +0100
+++ b/src/Pure/Tools/doc.scala	Sat Feb 27 19:57:36 2016 +0100
@@ -96,13 +96,20 @@
   def main(args: Array[String])
   {
     Command_Line.tool0 {
+      val getopts = Getopts(() => """
+Usage: isabelle doc [DOC ...]
+
+  View Isabelle documentation.
+""")
+      val docs = getopts(args)
+
       val entries = contents()
-      if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
+      if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
       else {
-        args.foreach(arg =>
-          entries.collectFirst { case Doc(name, _, path) if arg == name => path } match {
+        docs.foreach(doc =>
+          entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
             case Some(path) => view(path)
-            case None => error("No Isabelle documentation entry: " + quote(arg))
+            case None => error("No Isabelle documentation entry: " + quote(doc))
           }
         )
       }