# 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))