--- 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".
--- 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.
*}
--- 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%
%
--- /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[@]}" "$@"
+
--- 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 */