# HG changeset patch
# User wenzelm
# Date 1344268445 -7200
# Node ID 538ea0adb8e109b7d8c27dfe2a5cafc473c61af8
# Parent  db82a65cdb8018908ebe9e4032e43d4c50fe32bf# Parent  ceeea46bdeba4eb3e5eebd00b549e4ba41ceeef2
merged

diff -r db82a65cdb80 -r 538ea0adb8e1 NEWS
--- a/NEWS	Mon Aug 06 15:02:59 2012 +0100
+++ b/NEWS	Mon Aug 06 17:54:05 2012 +0200
@@ -85,6 +85,9 @@
 
   isabelle build -s -b HOLCF
 
+* The "isabelle options" tool prints Isabelle system options, as
+required for "isabelle build", for example.
+
 * The "isabelle mkroot" tool prepares session root directories for use
 with "isabelle build", similar to former "isabelle mkdir" for
 "isabelle usedir".
diff -r db82a65cdb80 -r 538ea0adb8e1 doc-src/System/Thy/Sessions.thy
--- a/doc-src/System/Thy/Sessions.thy	Mon Aug 06 15:02:59 2012 +0100
+++ b/doc-src/System/Thy/Sessions.thy	Mon Aug 06 17:54:05 2012 +0200
@@ -152,6 +152,30 @@
   the Isabelle distribution.  Isabelle/jEdit (\secref{sec:tool-jedit})
   includes a simple editing mode @{verbatim "isabelle-options"} for
   this file-format.
+
+  The @{tool_def options} tool prints Isabelle system options.  Its
+  command-line usage is:
+\begin{ttbox}
+Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
+
+  Options are:
+    -b           include $ISABELLE_BUILD_OPTIONS
+    -x FILE      export to FILE in YXML format
+
+  Print Isabelle system options, augmented by MORE_OPTIONS given as
+  arguments NAME=VAL or NAME.
+\end{ttbox}
+
+  The command line arguments provide additional system options of the
+  form @{text "name"}@{verbatim "="}@{text "value"} or @{text name}
+  for Boolean options.
+
+  Option @{verbatim "-b"} augments the implicit environment of system
+  options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\
+  \secref{sec:tool-build}.
+
+  Option @{verbatim "-x"} specifies a file to export the result in
+  YXML format, instead of printing it in human-readable form.
 *}
 
 
diff -r db82a65cdb80 -r 538ea0adb8e1 doc-src/System/Thy/document/Sessions.tex
--- a/doc-src/System/Thy/document/Sessions.tex	Mon Aug 06 15:02:59 2012 +0100
+++ b/doc-src/System/Thy/document/Sessions.tex	Mon Aug 06 17:54:05 2012 +0200
@@ -264,7 +264,31 @@
 See \verb|~~/etc/options| for the main defaults provided by
   the Isabelle distribution.  Isabelle/jEdit (\secref{sec:tool-jedit})
   includes a simple editing mode \verb|isabelle-options| for
-  this file-format.%
+  this file-format.
+
+  The \indexdef{}{tool}{options}\hypertarget{tool.options}{\hyperlink{tool.options}{\mbox{\isa{\isatool{options}}}}} tool prints Isabelle system options.  Its
+  command-line usage is:
+\begin{ttbox}
+Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
+
+  Options are:
+    -b           include $ISABELLE_BUILD_OPTIONS
+    -x FILE      export to FILE in YXML format
+
+  Print Isabelle system options, augmented by MORE_OPTIONS given as
+  arguments NAME=VAL or NAME.
+\end{ttbox}
+
+  The command line arguments provide additional system options of the
+  form \isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}value{\isaliteral{22}{\isachardoublequote}}} or \isa{name}
+  for Boolean options.
+
+  Option \verb|-b| augments the implicit environment of system
+  options by the ones of \hyperlink{setting.ISABELLE-BUILD-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BUILD{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}, cf.\
+  \secref{sec:tool-build}.
+
+  Option \verb|-x| specifies a file to export the result in
+  YXML format, instead of printing it in human-readable form.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r db82a65cdb80 -r 538ea0adb8e1 lib/Tools/options
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/options	Mon Aug 06 17:54:05 2012 +0200
@@ -0,0 +1,62 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: print Isabelle system options
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] [MORE_OPTIONS ...]"
+  echo
+  echo "  Options are:"
+  echo "    -b           include \$ISABELLE_BUILD_OPTIONS"
+  echo "    -x FILE      export to FILE in YXML format"
+  echo
+  echo "  Print Isabelle system options, augmented by MORE_OPTIONS given as"
+  echo "  arguments NAME=VAL or NAME."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+eval "declare -a BUILD_OPTIONS=()"
+EXPORT_FILE=""
+
+while getopts "bx:" OPT
+do
+  case "$OPT" in
+    b)
+      BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)
+      ;;
+    x)
+      EXPORT_FILE="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+## main
+
+[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
+
+exec "$ISABELLE_TOOL" java isabelle.Options "$EXPORT_FILE" "${BUILD_OPTIONS[@]}" "$@"
+
diff -r db82a65cdb80 -r 538ea0adb8e1 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Aug 06 15:02:59 2012 +0100
+++ b/src/Pure/System/options.scala	Mon Aug 06 17:54:05 2012 +0200
@@ -83,6 +83,25 @@
   /* encode */
 
   val encode: XML.Encode.T[Options] = (options => options.encode)
+
+
+  /* command line entry point */
+
+  def main(args: Array[String])
+  {
+    Command_Line.tool {
+      args.toList match {
+        case export_file :: more_options =>
+          val options = (Options.init() /: more_options)(_.define_simple(_))
+
+          if (export_file == "") java.lang.System.out.println(options.print)
+          else File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
+
+          0
+        case _ => error("Bad arguments:\n" + cat_lines(args))
+      }
+    }
+  }
 }
 
 
@@ -90,6 +109,12 @@
 {
   override def toString: String = options.iterator.mkString("Options (", ",", ")")
 
+  def print: String =
+    cat_lines(options.toList.sortBy(_._1).map({ case (name, opt) =>
+      name + " : " + opt.typ.print + " = " +
+        (if (opt.typ == Options.String) quote(opt.value) else opt.value) +
+      "\n  -- " + quote(opt.description) }))
+
 
   /* check */