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