prefer internal tool;
authorwenzelm
Sun Apr 03 22:36:11 2016 +0200 (2016-04-03)
changeset 62832c1410bcf6e87
parent 62831 5560905a32ae
child 62833 29dfa2ed9343
prefer internal tool;
lib/Tools/options
src/Pure/System/isabelle_tool.scala
src/Pure/System/options.scala
     1.1 --- a/lib/Tools/options	Sun Apr 03 22:31:16 2016 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,9 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# Author: Makarius
     1.7 -#
     1.8 -# DESCRIPTION: print Isabelle system options
     1.9 -
    1.10 -isabelle_admin_build jars || exit $?
    1.11 -
    1.12 -exec isabelle java isabelle.Options "$@"
     2.1 --- a/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:31:16 2016 +0200
     2.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:36:11 2016 +0200
     2.3 @@ -69,6 +69,7 @@
     2.4      }
     2.5  
     2.6    register(Doc.isabelle_tool)
     2.7 +  register(Options.isabelle_tool)
     2.8  
     2.9  
    2.10    /* command line entry point */
     3.1 --- a/src/Pure/System/options.scala	Sun Apr 03 22:31:16 2016 +0200
     3.2 +++ b/src/Pure/System/options.scala	Sun Apr 03 22:36:11 2016 +0200
     3.3 @@ -140,17 +140,16 @@
     3.4    val encode: XML.Encode.T[Options] = (options => options.encode)
     3.5  
     3.6  
     3.7 -  /* command line entry point */
     3.8 +  /* Isabelle tool wrapper */
     3.9  
    3.10 -  def main(args: Array[String])
    3.11 +  val isabelle_tool = Isabelle_Tool("option", "print Isabelle system options", args =>
    3.12    {
    3.13 -    Command_Line.tool0 {
    3.14 -      var build_options = false
    3.15 -      var get_option = ""
    3.16 -      var list_options = false
    3.17 -      var export_file = ""
    3.18 +    var build_options = false
    3.19 +    var get_option = ""
    3.20 +    var list_options = false
    3.21 +    var export_file = ""
    3.22  
    3.23 -      val getopts = Getopts("""
    3.24 +    val getopts = Getopts("""
    3.25  Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
    3.26  
    3.27    Options are:
    3.28 @@ -162,34 +161,33 @@
    3.29    Report Isabelle system options, augmented by MORE_OPTIONS given as
    3.30    arguments NAME=VAL or NAME.
    3.31  """,
    3.32 -        "b" -> (_ => build_options = true),
    3.33 -        "g:" -> (arg => get_option = arg),
    3.34 -        "l" -> (_ => list_options = true),
    3.35 -        "x:" -> (arg => export_file = arg))
    3.36 +      "b" -> (_ => build_options = true),
    3.37 +      "g:" -> (arg => get_option = arg),
    3.38 +      "l" -> (_ => list_options = true),
    3.39 +      "x:" -> (arg => export_file = arg))
    3.40  
    3.41 -      val more_options = getopts(args)
    3.42 -      if (get_option == "" && !list_options && export_file == "") getopts.usage()
    3.43 +    val more_options = getopts(args)
    3.44 +    if (get_option == "" && !list_options && export_file == "") getopts.usage()
    3.45  
    3.46 -      val options =
    3.47 -      {
    3.48 -        val options0 = Options.init()
    3.49 -        val options1 =
    3.50 -          if (build_options)
    3.51 -            (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
    3.52 -          else options0
    3.53 -        (options1 /: more_options)(_ + _)
    3.54 -      }
    3.55 +    val options =
    3.56 +    {
    3.57 +      val options0 = Options.init()
    3.58 +      val options1 =
    3.59 +        if (build_options)
    3.60 +          (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
    3.61 +        else options0
    3.62 +      (options1 /: more_options)(_ + _)
    3.63 +    }
    3.64  
    3.65 -      if (get_option != "")
    3.66 -        Console.println(options.check_name(get_option).value)
    3.67 +    if (get_option != "")
    3.68 +      Console.println(options.check_name(get_option).value)
    3.69  
    3.70 -      if (export_file != "")
    3.71 -        File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
    3.72 +    if (export_file != "")
    3.73 +      File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
    3.74  
    3.75 -      if (get_option == "" && export_file == "")
    3.76 -        Console.println(options.print)
    3.77 -    }
    3.78 -  }
    3.79 +    if (get_option == "" && export_file == "")
    3.80 +      Console.println(options.print)
    3.81 +  })
    3.82  }
    3.83  
    3.84