# HG changeset patch
# User wenzelm
# Date 1459715771 -7200
# Node ID c1410bcf6e87f78c34930d289e3b34e75b1df1a5
# Parent  5560905a32ae562448bf8828f5de46e232bf997c
prefer internal tool;

diff -r 5560905a32ae -r c1410bcf6e87 lib/Tools/options
--- 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 "$@"
diff -r 5560905a32ae -r c1410bcf6e87 src/Pure/System/isabelle_tool.scala
--- 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 */
diff -r 5560905a32ae -r c1410bcf6e87 src/Pure/System/options.scala
--- 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)
+  })
 }