--- a/lib/Tools/options Sun Apr 03 22:31:16 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: print Isabelle system options
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Options "$@"
--- a/src/Pure/System/isabelle_tool.scala Sun Apr 03 22:31:16 2016 +0200
+++ b/src/Pure/System/isabelle_tool.scala Sun Apr 03 22:36:11 2016 +0200
@@ -69,6 +69,7 @@
}
register(Doc.isabelle_tool)
+ register(Options.isabelle_tool)
/* command line entry point */
--- a/src/Pure/System/options.scala Sun Apr 03 22:31:16 2016 +0200
+++ b/src/Pure/System/options.scala Sun Apr 03 22:36:11 2016 +0200
@@ -140,17 +140,16 @@
val encode: XML.Encode.T[Options] = (options => options.encode)
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
+ val isabelle_tool = Isabelle_Tool("option", "print Isabelle system options", args =>
{
- Command_Line.tool0 {
- var build_options = false
- var get_option = ""
- var list_options = false
- var export_file = ""
+ var build_options = false
+ var get_option = ""
+ var list_options = false
+ var export_file = ""
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
Options are:
@@ -162,34 +161,33 @@
Report Isabelle system options, augmented by MORE_OPTIONS given as
arguments NAME=VAL or NAME.
""",
- "b" -> (_ => build_options = true),
- "g:" -> (arg => get_option = arg),
- "l" -> (_ => list_options = true),
- "x:" -> (arg => export_file = arg))
+ "b" -> (_ => build_options = true),
+ "g:" -> (arg => get_option = arg),
+ "l" -> (_ => list_options = true),
+ "x:" -> (arg => export_file = arg))
- val more_options = getopts(args)
- if (get_option == "" && !list_options && export_file == "") getopts.usage()
+ val more_options = getopts(args)
+ if (get_option == "" && !list_options && export_file == "") getopts.usage()
- val options =
- {
- val options0 = Options.init()
- val options1 =
- if (build_options)
- (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
- else options0
- (options1 /: more_options)(_ + _)
- }
+ val options =
+ {
+ val options0 = Options.init()
+ val options1 =
+ if (build_options)
+ (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
+ else options0
+ (options1 /: more_options)(_ + _)
+ }
- if (get_option != "")
- Console.println(options.check_name(get_option).value)
+ if (get_option != "")
+ Console.println(options.check_name(get_option).value)
- if (export_file != "")
- File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
+ if (export_file != "")
+ File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
- if (get_option == "" && export_file == "")
- Console.println(options.print)
- }
- }
+ if (get_option == "" && export_file == "")
+ Console.println(options.print)
+ })
}