"isabelle options" prints Isabelle system options;
authorwenzelm
Mon Aug 06 16:05:29 2012 +0200 (2012-08-06)
changeset 48693ceeea46bdeba
parent 48692 90e5093c3e1c
child 48697 538ea0adb8e1
"isabelle options" prints Isabelle system options;
NEWS
doc-src/System/Thy/Sessions.thy
doc-src/System/Thy/document/Sessions.tex
lib/Tools/options
src/Pure/System/options.scala
     1.1 --- a/NEWS	Mon Aug 06 14:33:23 2012 +0200
     1.2 +++ b/NEWS	Mon Aug 06 16:05:29 2012 +0200
     1.3 @@ -85,6 +85,9 @@
     1.4  
     1.5    isabelle build -s -b HOLCF
     1.6  
     1.7 +* The "isabelle options" tool prints Isabelle system options, as
     1.8 +required for "isabelle build", for example.
     1.9 +
    1.10  * The "isabelle mkroot" tool prepares session root directories for use
    1.11  with "isabelle build", similar to former "isabelle mkdir" for
    1.12  "isabelle usedir".
     2.1 --- a/doc-src/System/Thy/Sessions.thy	Mon Aug 06 14:33:23 2012 +0200
     2.2 +++ b/doc-src/System/Thy/Sessions.thy	Mon Aug 06 16:05:29 2012 +0200
     2.3 @@ -152,6 +152,30 @@
     2.4    the Isabelle distribution.  Isabelle/jEdit (\secref{sec:tool-jedit})
     2.5    includes a simple editing mode @{verbatim "isabelle-options"} for
     2.6    this file-format.
     2.7 +
     2.8 +  The @{tool_def options} tool prints Isabelle system options.  Its
     2.9 +  command-line usage is:
    2.10 +\begin{ttbox}
    2.11 +Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
    2.12 +
    2.13 +  Options are:
    2.14 +    -b           include $ISABELLE_BUILD_OPTIONS
    2.15 +    -x FILE      export to FILE in YXML format
    2.16 +
    2.17 +  Print Isabelle system options, augmented by MORE_OPTIONS given as
    2.18 +  arguments NAME=VAL or NAME.
    2.19 +\end{ttbox}
    2.20 +
    2.21 +  The command line arguments provide additional system options of the
    2.22 +  form @{text "name"}@{verbatim "="}@{text "value"} or @{text name}
    2.23 +  for Boolean options.
    2.24 +
    2.25 +  Option @{verbatim "-b"} augments the implicit environment of system
    2.26 +  options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\
    2.27 +  \secref{sec:tool-build}.
    2.28 +
    2.29 +  Option @{verbatim "-x"} specifies a file to export the result in
    2.30 +  YXML format, instead of printing it in human-readable form.
    2.31  *}
    2.32  
    2.33  
     3.1 --- a/doc-src/System/Thy/document/Sessions.tex	Mon Aug 06 14:33:23 2012 +0200
     3.2 +++ b/doc-src/System/Thy/document/Sessions.tex	Mon Aug 06 16:05:29 2012 +0200
     3.3 @@ -264,7 +264,31 @@
     3.4  See \verb|~~/etc/options| for the main defaults provided by
     3.5    the Isabelle distribution.  Isabelle/jEdit (\secref{sec:tool-jedit})
     3.6    includes a simple editing mode \verb|isabelle-options| for
     3.7 -  this file-format.%
     3.8 +  this file-format.
     3.9 +
    3.10 +  The \indexdef{}{tool}{options}\hypertarget{tool.options}{\hyperlink{tool.options}{\mbox{\isa{\isatool{options}}}}} tool prints Isabelle system options.  Its
    3.11 +  command-line usage is:
    3.12 +\begin{ttbox}
    3.13 +Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
    3.14 +
    3.15 +  Options are:
    3.16 +    -b           include $ISABELLE_BUILD_OPTIONS
    3.17 +    -x FILE      export to FILE in YXML format
    3.18 +
    3.19 +  Print Isabelle system options, augmented by MORE_OPTIONS given as
    3.20 +  arguments NAME=VAL or NAME.
    3.21 +\end{ttbox}
    3.22 +
    3.23 +  The command line arguments provide additional system options of the
    3.24 +  form \isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}value{\isaliteral{22}{\isachardoublequote}}} or \isa{name}
    3.25 +  for Boolean options.
    3.26 +
    3.27 +  Option \verb|-b| augments the implicit environment of system
    3.28 +  options by the ones of \hyperlink{setting.ISABELLE-BUILD-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BUILD{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}, cf.\
    3.29 +  \secref{sec:tool-build}.
    3.30 +
    3.31 +  Option \verb|-x| specifies a file to export the result in
    3.32 +  YXML format, instead of printing it in human-readable form.%
    3.33  \end{isamarkuptext}%
    3.34  \isamarkuptrue%
    3.35  %
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/lib/Tools/options	Mon Aug 06 16:05:29 2012 +0200
     4.3 @@ -0,0 +1,62 @@
     4.4 +#!/usr/bin/env bash
     4.5 +#
     4.6 +# Author: Makarius
     4.7 +#
     4.8 +# DESCRIPTION: print Isabelle system options
     4.9 +
    4.10 +
    4.11 +## diagnostics
    4.12 +
    4.13 +PRG="$(basename "$0")"
    4.14 +
    4.15 +function usage()
    4.16 +{
    4.17 +  echo
    4.18 +  echo "Usage: isabelle $PRG [OPTIONS] [MORE_OPTIONS ...]"
    4.19 +  echo
    4.20 +  echo "  Options are:"
    4.21 +  echo "    -b           include \$ISABELLE_BUILD_OPTIONS"
    4.22 +  echo "    -x FILE      export to FILE in YXML format"
    4.23 +  echo
    4.24 +  echo "  Print Isabelle system options, augmented by MORE_OPTIONS given as"
    4.25 +  echo "  arguments NAME=VAL or NAME."
    4.26 +  echo
    4.27 +  exit 1
    4.28 +}
    4.29 +
    4.30 +function fail()
    4.31 +{
    4.32 +  echo "$1" >&2
    4.33 +  exit 2
    4.34 +}
    4.35 +
    4.36 +
    4.37 +## process command line
    4.38 +
    4.39 +eval "declare -a BUILD_OPTIONS=()"
    4.40 +EXPORT_FILE=""
    4.41 +
    4.42 +while getopts "bx:" OPT
    4.43 +do
    4.44 +  case "$OPT" in
    4.45 +    b)
    4.46 +      BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)
    4.47 +      ;;
    4.48 +    x)
    4.49 +      EXPORT_FILE="$OPTARG"
    4.50 +      ;;
    4.51 +    \?)
    4.52 +      usage
    4.53 +      ;;
    4.54 +  esac
    4.55 +done
    4.56 +
    4.57 +shift $(($OPTIND - 1))
    4.58 +
    4.59 +
    4.60 +## main
    4.61 +
    4.62 +[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
    4.63 +
    4.64 +exec "$ISABELLE_TOOL" java isabelle.Options "$EXPORT_FILE" "${BUILD_OPTIONS[@]}" "$@"
    4.65 +
     5.1 --- a/src/Pure/System/options.scala	Mon Aug 06 14:33:23 2012 +0200
     5.2 +++ b/src/Pure/System/options.scala	Mon Aug 06 16:05:29 2012 +0200
     5.3 @@ -83,6 +83,25 @@
     5.4    /* encode */
     5.5  
     5.6    val encode: XML.Encode.T[Options] = (options => options.encode)
     5.7 +
     5.8 +
     5.9 +  /* command line entry point */
    5.10 +
    5.11 +  def main(args: Array[String])
    5.12 +  {
    5.13 +    Command_Line.tool {
    5.14 +      args.toList match {
    5.15 +        case export_file :: more_options =>
    5.16 +          val options = (Options.init() /: more_options)(_.define_simple(_))
    5.17 +
    5.18 +          if (export_file == "") java.lang.System.out.println(options.print)
    5.19 +          else File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
    5.20 +
    5.21 +          0
    5.22 +        case _ => error("Bad arguments:\n" + cat_lines(args))
    5.23 +      }
    5.24 +    }
    5.25 +  }
    5.26  }
    5.27  
    5.28  
    5.29 @@ -90,6 +109,12 @@
    5.30  {
    5.31    override def toString: String = options.iterator.mkString("Options (", ",", ")")
    5.32  
    5.33 +  def print: String =
    5.34 +    cat_lines(options.toList.sortBy(_._1).map({ case (name, opt) =>
    5.35 +      name + " : " + opt.typ.print + " = " +
    5.36 +        (if (opt.typ == Options.String) quote(opt.value) else opt.value) +
    5.37 +      "\n  -- " + quote(opt.description) }))
    5.38 +
    5.39  
    5.40    /* check */
    5.41