support isabelle options -g;
authorwenzelm
Sat Jul 27 16:59:25 2013 +0200 (2013-07-27)
changeset 52735842b5e7dcac8
parent 52734 077149654ab4
child 52736 317663b422bb
child 52737 7b396ef36af6
support isabelle options -g;
lib/Tools/options
src/Doc/System/Sessions.thy
src/Pure/System/options.scala
     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))