# HG changeset patch
# User wenzelm
# Date 1456668744 -3600
# Node ID 5b749c31eb97fb4b58d1cab1da4da1a33b296fa8
# Parent  91902961184c8685fd4696fa91e3cde1d3102b4a
moved getopts to Scala;

diff -r 91902961184c -r 5b749c31eb97 lib/Tools/update_header
--- a/lib/Tools/update_header	Sun Feb 28 15:00:17 2016 +0100
+++ b/lib/Tools/update_header	Sun Feb 28 15:12:24 2016 +0100
@@ -4,57 +4,6 @@
 #
 # DESCRIPTION: replace obsolete theory header command
 
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [FILES|DIRS...]"
-  echo
-  echo "  Options are:"
-  echo "    -s COMMAND   alternative heading command (default 'section')"
-  echo
-  echo "  Recursively find .thy files and replace obsolete theory header commands"
-  echo "  by 'section' (default), or 'chapter', 'subsection', 'subsubsection'."
-  echo
-  echo "  Old versions of files are preserved by appending \"~~\"."
-  echo
-  exit 1
-}
-
-
-## process command line
-
-#options
+isabelle_admin_build jars || exit $?
 
-SECTION="section"
-
-while getopts "s:" OPT
-do
-  case "$OPT" in
-    s)
-      SECTION="$OPTARG"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-find $SPECS -name \*.thy -print0 | \
-  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Header "$SECTION"
+"$ISABELLE_TOOL" java isabelle.Update_Header "$@"
diff -r 91902961184c -r 5b749c31eb97 src/Pure/Tools/update_header.scala
--- a/src/Pure/Tools/update_header.scala	Sun Feb 28 15:00:17 2016 +0100
+++ b/src/Pure/Tools/update_header.scala	Sun Feb 28 15:12:24 2016 +0100
@@ -31,14 +31,32 @@
   def main(args: Array[String])
   {
     Command_Line.tool0 {
-      args.toList match {
-        case section :: files =>
-          if (!headings.contains(section))
-            error("Bad heading command: " + quote(section))
-          files.foreach(file => update_header(section, Path.explode(file)))
-        case _ =>
-            error("Bad arguments:\n" + cat_lines(args))
-      }
+      var section = "section"
+
+      val getopts = Getopts(() => """
+Usage: isabelle update_header [FILES|DIRS...]
+
+  Options are:
+    -s COMMAND   alternative heading command (default 'section')
+
+  Recursively find .thy files and replace obsolete theory header commands
+  by 'chapter', 'section' (default), 'subsection', 'subsubsection',
+  'paragraph', 'subparagraph'.
+
+  Old versions of files are preserved by appending "~~".
+""",
+        "s:" -> (arg => section = arg))
+
+      val specs = getopts(args)
+      if (specs.isEmpty) getopts.usage()
+
+      if (!headings.contains(section))
+        error("Bad heading command: " + quote(section))
+
+      for {
+        spec <- specs
+        file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+      } update_header(section, Path.explode(File.standard_path(file)))
     }
   }
 }