# HG changeset patch # User wenzelm # Date 1374937165 -7200 # Node ID 842b5e7dcac8a3484e4621df0aae67fb5b836db3 # Parent 077149654ab4690d7446a63f14cc0a6f6130de89 support isabelle options -g; diff -r 077149654ab4 -r 842b5e7dcac8 lib/Tools/options --- a/lib/Tools/options Sat Jul 27 16:44:58 2013 +0200 +++ b/lib/Tools/options Sat Jul 27 16:59:25 2013 +0200 @@ -16,6 +16,7 @@ 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 @@ -35,15 +36,19 @@ ## process command line declare -a BUILD_OPTIONS=() +GET_OPTION="" LIST_OPTIONS="false" EXPORT_FILE="" -while getopts "blx:" OPT +while getopts "bg:lx:" OPT do case "$OPT" in b) eval "BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)" ;; + g) + GET_OPTION="$OPTARG" + ;; l) LIST_OPTIONS="true" ;; @@ -58,12 +63,13 @@ shift $(($OPTIND - 1)) -[ "$LIST_OPTIONS" = "false" -a -z "$EXPORT_FILE" ] && usage +[ -z "$GET_OPTION" -a "$LIST_OPTIONS" = "false" -a -z "$EXPORT_FILE" ] && usage ## main isabelle_admin_build jars || exit $? -exec "$ISABELLE_TOOL" java isabelle.Options "$EXPORT_FILE" "${BUILD_OPTIONS[@]}" "$@" +exec "$ISABELLE_TOOL" java isabelle.Options \ + "$GET_OPTION" "$EXPORT_FILE" "${BUILD_OPTIONS[@]}" "$@" diff -r 077149654ab4 -r 842b5e7dcac8 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Sat Jul 27 16:44:58 2013 +0200 +++ b/src/Doc/System/Sessions.thy Sat Jul 27 16:59:25 2013 +0200 @@ -232,6 +232,7 @@ Options are: -b include $ISABELLE_BUILD_OPTIONS + -g OPTION get value of OPTION -l list options -x FILE export to FILE in YXML format @@ -247,6 +248,8 @@ options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}. + Option @{verbatim "-g"} prints the value of the given option. + Option @{verbatim "-x"} specifies a file to export the result in YXML format, instead of printing it in human-readable form. *} diff -r 077149654ab4 -r 842b5e7dcac8 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sat Jul 27 16:44:58 2013 +0200 +++ b/src/Pure/System/options.scala Sat Jul 27 16:59:25 2013 +0200 @@ -137,11 +137,14 @@ { Command_Line.tool { args.toList match { - case export_file :: more_options => + case get_option :: export_file :: more_options => val options = (Options.init() /: more_options)(_ + _) - if (export_file == "") java.lang.System.out.println(options.print) - else File.write(Path.explode(export_file), YXML.string_of_body(options.encode)) + if (get_option != "") + java.lang.System.out.println(options.check_name(get_option).value) + else if (export_file != "") + File.write(Path.explode(export_file), YXML.string_of_body(options.encode)) + else java.lang.System.out.println(options.print) 0 case _ => error("Bad arguments:\n" + cat_lines(args))