src/Pure/System/options.scala
author wenzelm
Fri May 02 20:01:45 2014 +0200 (2014-05-02)
changeset 56831 e3ccf0809d51
parent 56631 89269bb8e7ca
child 58868 c5e1cce7ace3
permissions -rw-r--r--
prefer scala.Console with its support for thread-local redirection;
     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() + ":" + "=" + "--" +
    79       (SECTION, Keyword.THY_HEADING2) + (PUBLIC, Keyword.THY_DECL) + (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     val option_entry: Parser[Options => Options] =
    93     {
    94       command(SECTION) ~! text ^^
    95         { case _ ~ a => (options: Options) => options.set_section(a) } |
    96       opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
    97       keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
    98         { case a ~ pos ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
    99             (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
   100     }
   101 
   102     val prefs_entry: Parser[Options => Options] =
   103     {
   104       option_name ~ (keyword("=") ~! option_value) ^^
   105       { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) }
   106     }
   107 
   108     def parse_file(syntax: Outer_Syntax, parser: Parser[Options => Options],
   109       options: Options, file: Path): Options =
   110     {
   111       val toks = syntax.scan(File.read(file))
   112       val ops =
   113         parse_all(rep(parser), Token.reader(toks, file.implode)) match {
   114           case Success(result, _) => result
   115           case bad => error(bad.toString)
   116         }
   117       try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } }
   118       catch { case ERROR(msg) => error(msg + Position.here(file.position)) }
   119     }
   120   }
   121 
   122   def init_defaults(): Options =
   123   {
   124     var options = empty
   125     for {
   126       dir <- Isabelle_System.components()
   127       file = dir + OPTIONS if file.is_file
   128     } { options = Parser.parse_file(options_syntax, Parser.option_entry, options, file) }
   129     options
   130   }
   131 
   132   def init(): Options = init_defaults().load_prefs()
   133 
   134 
   135   /* encode */
   136 
   137   val encode: XML.Encode.T[Options] = (options => options.encode)
   138 
   139 
   140   /* command line entry point */
   141 
   142   def main(args: Array[String])
   143   {
   144     Command_Line.tool0 {
   145       args.toList match {
   146         case get_option :: export_file :: more_options =>
   147           val options = (Options.init() /: more_options)(_ + _)
   148 
   149           if (get_option != "")
   150             Console.println(options.check_name(get_option).value)
   151 
   152           if (export_file != "")
   153             File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
   154 
   155           if (get_option == "" && export_file == "")
   156             Console.println(options.print)
   157 
   158         case _ => error("Bad arguments:\n" + cat_lines(args))
   159       }
   160     }
   161   }
   162 }
   163 
   164 
   165 final class Options private(
   166   val options: Map[String, Options.Opt] = Map.empty,
   167   val section: String = "")
   168 {
   169   override def toString: String = options.iterator.mkString("Options (", ",", ")")
   170 
   171   private def print_opt(opt: Options.Opt): String =
   172     if (opt.public) "public " + opt.print else opt.print
   173 
   174   def print: String = cat_lines(options.toList.sortBy(_._1).map(p => print_opt(p._2)))
   175 
   176   def description(name: String): String = check_name(name).description
   177 
   178 
   179   /* check */
   180 
   181   def check_name(name: String): Options.Opt =
   182     options.get(name) match {
   183       case Some(opt) if !opt.unknown => opt
   184       case _ => error("Unknown option " + quote(name))
   185     }
   186 
   187   private def check_type(name: String, typ: Options.Type): Options.Opt =
   188   {
   189     val opt = check_name(name)
   190     if (opt.typ == typ) opt
   191     else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print)
   192   }
   193 
   194 
   195   /* basic operations */
   196 
   197   private def put[A](name: String, typ: Options.Type, value: String): Options =
   198   {
   199     val opt = check_type(name, typ)
   200     new Options(options + (name -> opt.copy(value = value)), section)
   201   }
   202 
   203   private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A =
   204   {
   205     val opt = check_type(name, typ)
   206     parse(opt.value) match {
   207       case Some(x) => x
   208       case None =>
   209         error("Malformed value for option " + quote(name) +
   210           " : " + typ.print + " =\n" + quote(opt.value))
   211     }
   212   }
   213 
   214 
   215   /* internal lookup and update */
   216 
   217   class Bool_Access
   218   {
   219     def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
   220     def update(name: String, x: Boolean): Options =
   221       put(name, Options.Bool, Properties.Value.Boolean(x))
   222   }
   223   val bool = new Bool_Access
   224 
   225   class Int_Access
   226   {
   227     def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
   228     def update(name: String, x: Int): Options =
   229       put(name, Options.Int, Properties.Value.Int(x))
   230   }
   231   val int = new Int_Access
   232 
   233   class Real_Access
   234   {
   235     def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
   236     def update(name: String, x: Double): Options =
   237       put(name, Options.Real, Properties.Value.Double(x))
   238   }
   239   val real = new Real_Access
   240 
   241   class String_Access
   242   {
   243     def apply(name: String): String = get(name, Options.String, s => Some(s))
   244     def update(name: String, x: String): Options = put(name, Options.String, x)
   245   }
   246   val string = new String_Access
   247 
   248   class Seconds_Access
   249   {
   250     def apply(name: String): Time = Time.seconds(real(name))
   251   }
   252   val seconds = new Seconds_Access
   253 
   254 
   255   /* external updates */
   256 
   257   private def check_value(name: String): Options =
   258   {
   259     val opt = check_name(name)
   260     opt.typ match {
   261       case Options.Bool => bool(name); this
   262       case Options.Int => int(name); this
   263       case Options.Real => real(name); this
   264       case Options.String => string(name); this
   265       case Options.Unknown => this
   266     }
   267   }
   268 
   269   def declare(
   270     public: Boolean,
   271     pos: Position.T,
   272     name: String,
   273     typ_name: String,
   274     value: String,
   275     description: String): Options =
   276   {
   277     options.get(name) match {
   278       case Some(other) =>
   279         error("Duplicate declaration of option " + quote(name) + Position.here(pos) +
   280           Position.here(other.pos))
   281       case None =>
   282         val typ =
   283           typ_name match {
   284             case "bool" => Options.Bool
   285             case "int" => Options.Int
   286             case "real" => Options.Real
   287             case "string" => Options.String
   288             case _ =>
   289               error("Unknown type for option " + quote(name) + " : " + quote(typ_name) +
   290                 Position.here(pos))
   291           }
   292         val opt = Options.Opt(public, pos, name, typ, value, value, description, section)
   293         (new Options(options + (name -> opt), section)).check_value(name)
   294     }
   295   }
   296 
   297   def add_permissive(name: String, value: String): Options =
   298   {
   299     if (options.isDefinedAt(name)) this + (name, value)
   300     else {
   301       val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, "", "")
   302       new Options(options + (name -> opt), section)
   303     }
   304   }
   305 
   306   def + (name: String, value: String): Options =
   307   {
   308     val opt = check_name(name)
   309     (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name)
   310   }
   311 
   312   def + (name: String, opt_value: Option[String]): Options =
   313   {
   314     val opt = check_name(name)
   315     opt_value match {
   316       case Some(value) => this + (name, value)
   317       case None if opt.typ == Options.Bool => this + (name, "true")
   318       case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
   319     }
   320   }
   321 
   322   def + (str: String): Options =
   323   {
   324     str.indexOf('=') match {
   325       case -1 => this + (str, None)
   326       case i => this + (str.substring(0, i), str.substring(i + 1))
   327     }
   328   }
   329 
   330   def ++ (specs: List[Options.Spec]): Options =
   331     (this /: specs)({ case (x, (y, z)) => x + (y, z) })
   332 
   333 
   334   /* sections */
   335 
   336   def set_section(new_section: String): Options =
   337     new Options(options, new_section)
   338 
   339   def sections: List[(String, List[Options.Opt])] =
   340     options.groupBy(_._2.section).toList.map({ case (a, opts) => (a, opts.toList.map(_._2)) })
   341 
   342 
   343   /* encode */
   344 
   345   def encode: XML.Body =
   346   {
   347     val opts =
   348       for ((_, opt) <- options.toList; if !opt.unknown)
   349         yield (opt.pos, (opt.name, (opt.typ.print, opt.value)))
   350 
   351     import XML.Encode.{string => string_, _}
   352     list(pair(properties, pair(string_, pair(string_, string_))))(opts)
   353   }
   354 
   355 
   356   /* user preferences */
   357 
   358   def load_prefs(): Options =
   359     if (Options.PREFS.is_file)
   360       Options.Parser.parse_file(
   361         Options.prefs_syntax, Options.Parser.prefs_entry, this, Options.PREFS)
   362     else this
   363 
   364   def save_prefs()
   365   {
   366     val defaults = Options.init_defaults()
   367     val changed =
   368       (for {
   369         (name, opt2) <- options.iterator
   370         opt1 = defaults.options.get(name)
   371         if (opt1.isEmpty || opt1.get.value != opt2.value)
   372       } yield (name, opt2.value, if (opt1.isEmpty) "  (* unknown *)" else "")).toList
   373 
   374     val prefs =
   375       changed.sortBy(_._1)
   376         .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
   377 
   378     Isabelle_System.mkdirs(Options.PREFS_DIR)
   379     File.write_backup(Options.PREFS,
   380       "(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs)
   381   }
   382 }
   383 
   384 
   385 class Options_Variable
   386 {
   387   private var options = Options.empty
   388 
   389   def value: Options = synchronized { options }
   390   def update(new_options: Options): Unit = synchronized { options = new_options }
   391 
   392   def + (name: String, x: String): Unit = synchronized { options = options + (name, x) }
   393 
   394   class Bool_Access
   395   {
   396     def apply(name: String): Boolean = synchronized { options.bool(name) }
   397     def update(name: String, x: Boolean): Unit =
   398       synchronized { options = options.bool.update(name, x) }
   399   }
   400   val bool = new Bool_Access
   401 
   402   class Int_Access
   403   {
   404     def apply(name: String): Int = synchronized { options.int(name) }
   405     def update(name: String, x: Int): Unit =
   406       synchronized { options = options.int.update(name, x) }
   407   }
   408   val int = new Int_Access
   409 
   410   class Real_Access
   411   {
   412     def apply(name: String): Double = synchronized { options.real(name) }
   413     def update(name: String, x: Double): Unit =
   414       synchronized { options = options.real.update(name, x) }
   415   }
   416   val real = new Real_Access
   417 
   418   class String_Access
   419   {
   420     def apply(name: String): String = synchronized { options.string(name) }
   421     def update(name: String, x: String): Unit =
   422       synchronized { options = options.string.update(name, x) }
   423   }
   424   val string = new String_Access
   425 
   426   class Seconds_Access
   427   {
   428     def apply(name: String): Time = synchronized { options.seconds(name) }
   429   }
   430   val seconds = new Seconds_Access
   431 }
   432