# HG changeset patch # User wenzelm # Date 1456669569 -3600 # Node ID 1785cbadd22695428ba469d52e380e8c078ef643 # Parent 5ec1d01089e355f87b6167028943d98abf7744a8 moved getopts to Scala; diff -r 5ec1d01089e3 -r 1785cbadd226 lib/Tools/update_then --- a/lib/Tools/update_then Sun Feb 28 15:21:08 2016 +0100 +++ b/lib/Tools/update_then Sun Feb 28 15:26:09 2016 +0100 @@ -4,35 +4,6 @@ # # DESCRIPTION: expand old Isar command conflations 'hence' and 'thus' - -## diagnostics - -PRG="$(basename "$0")" +isabelle_admin_build jars || exit $? -function usage() -{ - echo - echo "Usage: isabelle $PRG [FILES|DIRS...]" - echo - echo " Recursively find .thy files and expand old Isar command conflations:" - echo - echo " hence ~> then have" - echo " thus ~> then show" - echo - echo " Old versions of files are preserved by appending \"~~\"." - echo - exit 1 -} - - -## process command line - -[ "$#" -eq 0 -o "$1" = "-?" ] && usage - -SPECS="$@"; shift "$#" - - -## main - -find $SPECS -name \*.thy -print0 | \ - xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Then +"$ISABELLE_TOOL" java isabelle.Update_Then "$@" diff -r 5ec1d01089e3 -r 1785cbadd226 src/Pure/Tools/update_then.scala --- a/src/Pure/Tools/update_then.scala Sun Feb 28 15:21:08 2016 +0100 +++ b/src/Pure/Tools/update_then.scala Sun Feb 28 15:26:09 2016 +0100 @@ -33,7 +33,24 @@ def main(args: Array[String]) { Command_Line.tool0 { - args.foreach(arg => update_then(Path.explode(arg))) + val getopts = Getopts(() => """ +Usage: isabelle update_then [FILES|DIRS...] + + Recursively find .thy files and expand old Isar command conflations: + + hence ~> then have + thus ~> then show + + Old versions of files are preserved by appending "~~". +""") + + val specs = getopts(args) + if (specs.isEmpty) getopts.usage() + + for { + spec <- specs + file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy")) + } update_then(Path.explode(File.standard_path(file))) } } }