1.1 --- a/lib/Tools/options Sat Jul 27 16:44:58 2013 +0200
1.2 +++ b/lib/Tools/options Sat Jul 27 16:59:25 2013 +0200
1.3 @@ -16,6 +16,7 @@
1.4 echo
1.5 echo " Options are:"
1.6 echo " -b include \$ISABELLE_BUILD_OPTIONS"
1.7 + echo " -g OPTION get value of OPTION"
1.8 echo " -l list options"
1.9 echo " -x FILE export options to FILE in YXML format"
1.10 echo
1.11 @@ -35,15 +36,19 @@
1.12 ## process command line
1.13
1.14 declare -a BUILD_OPTIONS=()
1.15 +GET_OPTION=""
1.16 LIST_OPTIONS="false"
1.17 EXPORT_FILE=""
1.18
1.19 -while getopts "blx:" OPT
1.20 +while getopts "bg:lx:" OPT
1.21 do
1.22 case "$OPT" in
1.23 b)
1.24 eval "BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
1.25 ;;
1.26 + g)
1.27 + GET_OPTION="$OPTARG"
1.28 + ;;
1.29 l)
1.30 LIST_OPTIONS="true"
1.31 ;;
1.32 @@ -58,12 +63,13 @@
1.33
1.34 shift $(($OPTIND - 1))
1.35
1.36 -[ "$LIST_OPTIONS" = "false" -a -z "$EXPORT_FILE" ] && usage
1.37 +[ -z "$GET_OPTION" -a "$LIST_OPTIONS" = "false" -a -z "$EXPORT_FILE" ] && usage
1.38
1.39
1.40 ## main
1.41
1.42 isabelle_admin_build jars || exit $?
1.43
1.44 -exec "$ISABELLE_TOOL" java isabelle.Options "$EXPORT_FILE" "${BUILD_OPTIONS[@]}" "$@"
1.45 +exec "$ISABELLE_TOOL" java isabelle.Options \
1.46 + "$GET_OPTION" "$EXPORT_FILE" "${BUILD_OPTIONS[@]}" "$@"
1.47
2.1 --- a/src/Doc/System/Sessions.thy Sat Jul 27 16:44:58 2013 +0200
2.2 +++ b/src/Doc/System/Sessions.thy Sat Jul 27 16:59:25 2013 +0200
2.3 @@ -232,6 +232,7 @@
2.4
2.5 Options are:
2.6 -b include $ISABELLE_BUILD_OPTIONS
2.7 + -g OPTION get value of OPTION
2.8 -l list options
2.9 -x FILE export to FILE in YXML format
2.10
2.11 @@ -247,6 +248,8 @@
2.12 options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\
2.13 \secref{sec:tool-build}.
2.14
2.15 + Option @{verbatim "-g"} prints the value of the given option.
2.16 +
2.17 Option @{verbatim "-x"} specifies a file to export the result in
2.18 YXML format, instead of printing it in human-readable form.
2.19 *}
3.1 --- a/src/Pure/System/options.scala Sat Jul 27 16:44:58 2013 +0200
3.2 +++ b/src/Pure/System/options.scala Sat Jul 27 16:59:25 2013 +0200
3.3 @@ -137,11 +137,14 @@
3.4 {
3.5 Command_Line.tool {
3.6 args.toList match {
3.7 - case export_file :: more_options =>
3.8 + case get_option :: export_file :: more_options =>
3.9 val options = (Options.init() /: more_options)(_ + _)
3.10
3.11 - if (export_file == "") java.lang.System.out.println(options.print)
3.12 - else File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
3.13 + if (get_option != "")
3.14 + java.lang.System.out.println(options.check_name(get_option).value)
3.15 + else if (export_file != "")
3.16 + File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
3.17 + else java.lang.System.out.println(options.print)
3.18
3.19 0
3.20 case _ => error("Bad arguments:\n" + cat_lines(args))