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)
+  })
 }