src/Pure/System/options.scala
author wenzelm
Sun Apr 03 22:36:11 2016 +0200 (2016-04-03)
changeset 62832 c1410bcf6e87
parent 62454 38c89353b349
child 62968 4e4738698db4
permissions -rw-r--r--
prefer internal tool;
     1 /*  Title:      Pure/System/options.scala
     2     Author:     Makarius
     3 
     4 System options with external string representation.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.util.Calendar
    11 
    12 
    13 object Options
    14 {
    15   type Spec = (String, Option[String])
    16 
    17   val empty: Options = new Options()
    18 
    19 
    20   /* representation */
    21 
    22   sealed abstract class Type
    23   {
    24     def print: String = Word.lowercase(toString)
    25   }
    26   case object Bool extends Type
    27   case object Int extends Type
    28   case object Real extends Type
    29   case object String extends Type
    30   case object Unknown extends Type
    31 
    32   case class Opt(
    33     public: Boolean,
    34     pos: Position.T,
    35     name: String,
    36     typ: Type,
    37     value: String,
    38     default_value: String,
    39     description: String,
    40     section: String)
    41   {
    42     private def print(default: Boolean): String =
    43     {
    44       val x = if (default) default_value else value
    45       "option " + name + " : " + typ.print + " = " +
    46         (if (typ == Options.String) quote(x) else x) +
    47         (if (description == "") "" else "\n  -- " + quote(description))
    48     }
    49 
    50     def print: String = print(false)
    51     def print_default: String = print(true)
    52 
    53     def title(strip: String = ""): String =
    54     {
    55       val words = Word.explode('_', name)
    56       val words1 =
    57         words match {
    58           case word :: rest if word == strip => rest
    59           case _ => words
    60         }
    61       Word.implode(words1.map(Word.perhaps_capitalize(_)))
    62     }
    63 
    64     def unknown: Boolean = typ == Unknown
    65   }
    66 
    67 
    68   /* parsing */
    69 
    70   private val SECTION = "section"
    71   private val PUBLIC = "public"
    72   private val OPTION = "option"
    73   private val OPTIONS = Path.explode("etc/options")
    74   private val PREFS_DIR = Path.explode("$ISABELLE_HOME_USER/etc")
    75   private val PREFS = PREFS_DIR + Path.basic("preferences")
    76 
    77   lazy val options_syntax =
    78     Outer_Syntax.init() + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
    79       (SECTION, Keyword.DOCUMENT_HEADING) + PUBLIC + (OPTION, Keyword.THY_DECL)
    80 
    81   lazy val prefs_syntax = Outer_Syntax.init() + "="
    82 
    83   object Parser extends Parse.Parser
    84   {
    85     val option_name = atom("option name", _.is_xname)
    86     val option_type = atom("option type", _.is_ident)
    87     val option_value =
    88       opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
    89         { case s ~ n => if (s.isDefined) "-" + n else n } |
    90       atom("option value", tok => tok.is_name || tok.is_float)
    91 
    92     def comment_marker: Parser[String] =
    93       $$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded)
    94 
    95     val option_entry: Parser[Options => Options] =
    96     {
    97       command(SECTION) ~! text ^^
    98         { case _ ~ a => (options: Options) => options.set_section(a) } |
    99       opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~
   100       $$$("=") ~ option_value ~ (comment_marker ~! text ^^ { case _ ~ x => x } | success(""))) ^^
   101         { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e) =>
   102             (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
   103     }
   104 
   105     val prefs_entry: Parser[Options => Options] =
   106     {
   107       option_name ~ ($$$("=") ~! option_value) ^^
   108       { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) }
   109     }
   110 
   111     def parse_file(syntax: Outer_Syntax, parser: Parser[Options => Options],
   112       options: Options, file: Path): Options =
   113     {
   114       val toks = Token.explode(syntax.keywords, File.read(file))
   115       val ops =
   116         parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file.implode))) match {
   117           case Success(result, _) => result
   118           case bad => error(bad.toString)
   119         }
   120       try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } }
   121       catch { case ERROR(msg) => error(msg + Position.here(file.position)) }
   122     }
   123   }
   124 
   125   def init_defaults(): Options =
   126   {
   127     var options = empty
   128     for {
   129       dir <- Isabelle_System.components()
   130       file = dir + OPTIONS if file.is_file
   131     } { options = Parser.parse_file(options_syntax, Parser.option_entry, options, file) }
   132     options
   133   }
   134 
   135   def init(): Options = init_defaults().load_prefs()
   136 
   137 
   138   /* encode */
   139 
   140   val encode: XML.Encode.T[Options] = (options => options.encode)
   141 
   142 
   143   /* Isabelle tool wrapper */
   144 
   145   val isabelle_tool = Isabelle_Tool("option", "print Isabelle system options", args =>
   146   {
   147     var build_options = false
   148     var get_option = ""
   149     var list_options = false
   150     var export_file = ""
   151 
   152     val getopts = Getopts("""
   153 Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
   154 
   155   Options are:
   156     -b           include $ISABELLE_BUILD_OPTIONS
   157     -g OPTION    get value of OPTION
   158     -l           list options
   159     -x FILE      export options to FILE in YXML format
   160 
   161   Report Isabelle system options, augmented by MORE_OPTIONS given as
   162   arguments NAME=VAL or NAME.
   163 """,
   164       "b" -> (_ => build_options = true),
   165       "g:" -> (arg => get_option = arg),
   166       "l" -> (_ => list_options = true),
   167       "x:" -> (arg => export_file = arg))
   168 
   169     val more_options = getopts(args)
   170     if (get_option == "" && !list_options && export_file == "") getopts.usage()
   171 
   172     val options =
   173     {
   174       val options0 = Options.init()
   175       val options1 =
   176         if (build_options)
   177           (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
   178         else options0
   179       (options1 /: more_options)(_ + _)
   180     }
   181 
   182     if (get_option != "")
   183       Console.println(options.check_name(get_option).value)
   184 
   185     if (export_file != "")
   186       File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
   187 
   188     if (get_option == "" && export_file == "")
   189       Console.println(options.print)
   190   })
   191 }
   192 
   193 
   194 final class Options private(
   195   val options: Map[String, Options.Opt] = Map.empty,
   196   val section: String = "")
   197 {
   198   override def toString: String = options.iterator.mkString("Options (", ",", ")")
   199 
   200   private def print_opt(opt: Options.Opt): String =
   201     if (opt.public) "public " + opt.print else opt.print
   202 
   203   def print: String = cat_lines(options.toList.sortBy(_._1).map(p => print_opt(p._2)))
   204 
   205   def description(name: String): String = check_name(name).description
   206 
   207 
   208   /* check */
   209 
   210   def check_name(name: String): Options.Opt =
   211     options.get(name) match {
   212       case Some(opt) if !opt.unknown => opt
   213       case _ => error("Unknown option " + quote(name))
   214     }
   215 
   216   private def check_type(name: String, typ: Options.Type): Options.Opt =
   217   {
   218     val opt = check_name(name)
   219     if (opt.typ == typ) opt
   220     else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print)
   221   }
   222 
   223 
   224   /* basic operations */
   225 
   226   private def put[A](name: String, typ: Options.Type, value: String): Options =
   227   {
   228     val opt = check_type(name, typ)
   229     new Options(options + (name -> opt.copy(value = value)), section)
   230   }
   231 
   232   private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A =
   233   {
   234     val opt = check_type(name, typ)
   235     parse(opt.value) match {
   236       case Some(x) => x
   237       case None =>
   238         error("Malformed value for option " + quote(name) +
   239           " : " + typ.print + " =\n" + quote(opt.value))
   240     }
   241   }
   242 
   243 
   244   /* internal lookup and update */
   245 
   246   class Bool_Access
   247   {
   248     def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
   249     def update(name: String, x: Boolean): Options =
   250       put(name, Options.Bool, Properties.Value.Boolean(x))
   251   }
   252   val bool = new Bool_Access
   253 
   254   class Int_Access
   255   {
   256     def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
   257     def update(name: String, x: Int): Options =
   258       put(name, Options.Int, Properties.Value.Int(x))
   259   }
   260   val int = new Int_Access
   261 
   262   class Real_Access
   263   {
   264     def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
   265     def update(name: String, x: Double): Options =
   266       put(name, Options.Real, Properties.Value.Double(x))
   267   }
   268   val real = new Real_Access
   269 
   270   class String_Access
   271   {
   272     def apply(name: String): String = get(name, Options.String, s => Some(s))
   273     def update(name: String, x: String): Options = put(name, Options.String, x)
   274   }
   275   val string = new String_Access
   276 
   277   class Seconds_Access
   278   {
   279     def apply(name: String): Time = Time.seconds(real(name))
   280   }
   281   val seconds = new Seconds_Access
   282 
   283 
   284   /* external updates */
   285 
   286   private def check_value(name: String): Options =
   287   {
   288     val opt = check_name(name)
   289     opt.typ match {
   290       case Options.Bool => bool(name); this
   291       case Options.Int => int(name); this
   292       case Options.Real => real(name); this
   293       case Options.String => string(name); this
   294       case Options.Unknown => this
   295     }
   296   }
   297 
   298   def declare(
   299     public: Boolean,
   300     pos: Position.T,
   301     name: String,
   302     typ_name: String,
   303     value: String,
   304     description: String): Options =
   305   {
   306     options.get(name) match {
   307       case Some(other) =>
   308         error("Duplicate declaration of option " + quote(name) + Position.here(pos) +
   309           Position.here(other.pos))
   310       case None =>
   311         val typ =
   312           typ_name match {
   313             case "bool" => Options.Bool
   314             case "int" => Options.Int
   315             case "real" => Options.Real
   316             case "string" => Options.String
   317             case _ =>
   318               error("Unknown type for option " + quote(name) + " : " + quote(typ_name) +
   319                 Position.here(pos))
   320           }
   321         val opt = Options.Opt(public, pos, name, typ, value, value, description, section)
   322         (new Options(options + (name -> opt), section)).check_value(name)
   323     }
   324   }
   325 
   326   def add_permissive(name: String, value: String): Options =
   327   {
   328     if (options.isDefinedAt(name)) this + (name, value)
   329     else {
   330       val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, "", "")
   331       new Options(options + (name -> opt), section)
   332     }
   333   }
   334 
   335   def + (name: String, value: String): Options =
   336   {
   337     val opt = check_name(name)
   338     (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name)
   339   }
   340 
   341   def + (name: String, opt_value: Option[String]): Options =
   342   {
   343     val opt = check_name(name)
   344     opt_value match {
   345       case Some(value) => this + (name, value)
   346       case None if opt.typ == Options.Bool => this + (name, "true")
   347       case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
   348     }
   349   }
   350 
   351   def + (str: String): Options =
   352   {
   353     str.indexOf('=') match {
   354       case -1 => this + (str, None)
   355       case i => this + (str.substring(0, i), str.substring(i + 1))
   356     }
   357   }
   358 
   359   def ++ (specs: List[Options.Spec]): Options =
   360     (this /: specs)({ case (x, (y, z)) => x + (y, z) })
   361 
   362 
   363   /* sections */
   364 
   365   def set_section(new_section: String): Options =
   366     new Options(options, new_section)
   367 
   368   def sections: List[(String, List[Options.Opt])] =
   369     options.groupBy(_._2.section).toList.map({ case (a, opts) => (a, opts.toList.map(_._2)) })
   370 
   371 
   372   /* encode */
   373 
   374   def encode: XML.Body =
   375   {
   376     val opts =
   377       for ((_, opt) <- options.toList; if !opt.unknown)
   378         yield (opt.pos, (opt.name, (opt.typ.print, opt.value)))
   379 
   380     import XML.Encode.{string => string_, _}
   381     list(pair(properties, pair(string_, pair(string_, string_))))(opts)
   382   }
   383 
   384 
   385   /* user preferences */
   386 
   387   def load_prefs(): Options =
   388     if (Options.PREFS.is_file)
   389       Options.Parser.parse_file(
   390         Options.prefs_syntax, Options.Parser.prefs_entry, this, Options.PREFS)
   391     else this
   392 
   393   def save_prefs()
   394   {
   395     val defaults = Options.init_defaults()
   396     val changed =
   397       (for {
   398         (name, opt2) <- options.iterator
   399         opt1 = defaults.options.get(name)
   400         if opt1.isEmpty || opt1.get.value != opt2.value
   401       } yield (name, opt2.value, if (opt1.isEmpty) "  (* unknown *)" else "")).toList
   402 
   403     val prefs =
   404       changed.sortBy(_._1)
   405         .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
   406 
   407     Isabelle_System.mkdirs(Options.PREFS_DIR)
   408     File.write_backup(Options.PREFS,
   409       "(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs)
   410   }
   411 }
   412 
   413 
   414 class Options_Variable
   415 {
   416   private var options: Option[Options] = None
   417 
   418   def store(new_options: Options): Unit = synchronized { options = Some(new_options) }
   419 
   420   def value: Options = synchronized {
   421     options match {
   422       case Some(opts) => opts
   423       case None => error("Uninitialized Isabelle system options")
   424     }
   425   }
   426 
   427   private def upd(f: Options => Options): Unit = synchronized { options = Some(f(value)) }
   428 
   429   def + (name: String, x: String): Unit = upd(opts => opts + (name, x))
   430 
   431   class Bool_Access
   432   {
   433     def apply(name: String): Boolean = value.bool(name)
   434     def update(name: String, x: Boolean): Unit = upd(opts => opts.bool.update(name, x))
   435   }
   436   val bool = new Bool_Access
   437 
   438   class Int_Access
   439   {
   440     def apply(name: String): Int = value.int(name)
   441     def update(name: String, x: Int): Unit = upd(opts => opts.int.update(name, x))
   442   }
   443   val int = new Int_Access
   444 
   445   class Real_Access
   446   {
   447     def apply(name: String): Double = value.real(name)
   448     def update(name: String, x: Double): Unit = upd(opts => opts.real.update(name, x))
   449   }
   450   val real = new Real_Access
   451 
   452   class String_Access
   453   {
   454     def apply(name: String): String = value.string(name)
   455     def update(name: String, x: String): Unit = upd(opts => opts.string.update(name, x))
   456   }
   457   val string = new String_Access
   458 
   459   class Seconds_Access
   460   {
   461     def apply(name: String): Time = value.seconds(name)
   462   }
   463   val seconds = new Seconds_Access
   464 }