src/Pure/System/options.scala
author wenzelm
Tue Sep 11 23:26:03 2012 +0200 (2012-09-11)
changeset 49296 313369027391
parent 49295 2750756db9c5
child 49954 44658062d822
permissions -rw-r--r--
some GUI support for color options;
     1 /*  Title:      Pure/System/options.scala
     2     Author:     Makarius
     3 
     4 Stand-alone options with external string representation.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.util.Locale
    11 import java.util.Calendar
    12 
    13 
    14 object Options
    15 {
    16   type Spec = (String, Option[String])
    17 
    18   val empty: Options = new Options()
    19 
    20 
    21   /* representation */
    22 
    23   sealed abstract class Type
    24   {
    25     def print: String = toString.toLowerCase(Locale.ENGLISH)
    26   }
    27   case object Bool extends Type
    28   case object Int extends Type
    29   case object Real extends Type
    30   case object String extends Type
    31   case object Unknown extends Type
    32 
    33   case class Opt(name: String, typ: Type, value: String, default_value: String,
    34     description: String, section: String)
    35   {
    36     private def print(default: Boolean): String =
    37     {
    38       val x = if (default) default_value else value
    39       "option " + name + " : " + typ.print + " = " +
    40         (if (typ == Options.String) quote(x) else x) +
    41         (if (description == "") "" else "\n  -- " + quote(description))
    42     }
    43 
    44     def print: String = print(false)
    45     def print_default: String = print(true)
    46 
    47     def title(strip: String): String =
    48     {
    49       val words = space_explode('_', name)
    50       val words1 =
    51         words match {
    52           case word :: rest if word == strip => rest
    53           case _ => words
    54         }
    55       words1.map(Library.capitalize).mkString(" ")
    56     }
    57 
    58     def unknown: Boolean = typ == Unknown
    59   }
    60 
    61 
    62   /* parsing */
    63 
    64   private val SECTION = "section"
    65   private val OPTION = "option"
    66   private val OPTIONS = Path.explode("etc/options")
    67   private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences")
    68   private val PREFS_BACKUP = Path.explode("$ISABELLE_HOME_USER/etc/preferences~")
    69 
    70   lazy val options_syntax =
    71     Outer_Syntax.init() + ":" + "=" + "--" +
    72       (SECTION, Keyword.THY_HEADING2) + (OPTION, Keyword.THY_DECL)
    73 
    74   lazy val prefs_syntax = Outer_Syntax.init() + "="
    75 
    76   object Parser extends Parse.Parser
    77   {
    78     val option_name = atom("option name", _.is_xname)
    79     val option_type = atom("option type", _.is_ident)
    80     val option_value =
    81       opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
    82         { case s ~ n => if (s.isDefined) "-" + n else n } |
    83       atom("option value", tok => tok.is_name || tok.is_float)
    84 
    85     val option_entry: Parser[Options => Options] =
    86     {
    87       command(SECTION) ~! text ^^
    88         { case _ ~ a => (options: Options) => options.set_section(a) } |
    89       command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
    90       keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
    91         { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) }
    92     }
    93 
    94     val prefs_entry: Parser[Options => Options] =
    95     {
    96       option_name ~ (keyword("=") ~! option_value) ^^
    97       { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) }
    98     }
    99 
   100     def parse_file(syntax: Outer_Syntax, parser: Parser[Options => Options],
   101       options: Options, file: Path): Options =
   102     {
   103       val toks = syntax.scan(File.read(file))
   104       val ops =
   105         parse_all(rep(parser), Token.reader(toks, file.implode)) match {
   106           case Success(result, _) => result
   107           case bad => error(bad.toString)
   108         }
   109       try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } }
   110       catch { case ERROR(msg) => error(msg + Position.here(file.position)) }
   111     }
   112   }
   113 
   114   def init_defaults(): Options =
   115   {
   116     var options = empty
   117     for {
   118       dir <- Isabelle_System.components()
   119       file = dir + OPTIONS if file.is_file
   120     } { options = Parser.parse_file(options_syntax, Parser.option_entry, options, file) }
   121     options
   122   }
   123 
   124   def init(): Options = init_defaults().load_prefs()
   125 
   126 
   127   /* encode */
   128 
   129   val encode: XML.Encode.T[Options] = (options => options.encode)
   130 
   131 
   132   /* command line entry point */
   133 
   134   def main(args: Array[String])
   135   {
   136     Command_Line.tool {
   137       args.toList match {
   138         case export_file :: more_options =>
   139           val options = (Options.init() /: more_options)(_ + _)
   140 
   141           if (export_file == "") java.lang.System.out.println(options.print)
   142           else File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
   143 
   144           0
   145         case _ => error("Bad arguments:\n" + cat_lines(args))
   146       }
   147     }
   148   }
   149 }
   150 
   151 
   152 final class Options private(
   153   val options: Map[String, Options.Opt] = Map.empty,
   154   val section: String = "")
   155 {
   156   override def toString: String = options.iterator.mkString("Options (", ",", ")")
   157 
   158   def print: String = cat_lines(options.toList.sortBy(_._1).map(p => p._2.print))
   159 
   160   def description(name: String): String = check_name(name).description
   161 
   162 
   163   /* check */
   164 
   165   def check_name(name: String): Options.Opt =
   166     options.get(name) match {
   167       case Some(opt) if !opt.unknown => opt
   168       case _ => error("Unknown option " + quote(name))
   169     }
   170 
   171   private def check_type(name: String, typ: Options.Type): Options.Opt =
   172   {
   173     val opt = check_name(name)
   174     if (opt.typ == typ) opt
   175     else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print)
   176   }
   177 
   178 
   179   /* basic operations */
   180 
   181   private def put[A](name: String, typ: Options.Type, value: String): Options =
   182   {
   183     val opt = check_type(name, typ)
   184     new Options(options + (name -> opt.copy(value = value)), section)
   185   }
   186 
   187   private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A =
   188   {
   189     val opt = check_type(name, typ)
   190     parse(opt.value) match {
   191       case Some(x) => x
   192       case None =>
   193         error("Malformed value for option " + quote(name) +
   194           " : " + typ.print + " =\n" + quote(opt.value))
   195     }
   196   }
   197 
   198 
   199   /* internal lookup and update */
   200 
   201   val bool = new Object
   202   {
   203     def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
   204     def update(name: String, x: Boolean): Options =
   205       put(name, Options.Bool, Properties.Value.Boolean(x))
   206   }
   207 
   208   val int = new Object
   209   {
   210     def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
   211     def update(name: String, x: Int): Options =
   212       put(name, Options.Int, Properties.Value.Int(x))
   213   }
   214 
   215   val real = new Object
   216   {
   217     def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
   218     def update(name: String, x: Double): Options =
   219       put(name, Options.Real, Properties.Value.Double(x))
   220   }
   221 
   222   val string = new Object
   223   {
   224     def apply(name: String): String = get(name, Options.String, s => Some(s))
   225     def update(name: String, x: String): Options = put(name, Options.String, x)
   226   }
   227 
   228 
   229   /* external updates */
   230 
   231   private def check_value(name: String): Options =
   232   {
   233     val opt = check_name(name)
   234     opt.typ match {
   235       case Options.Bool => bool(name); this
   236       case Options.Int => int(name); this
   237       case Options.Real => real(name); this
   238       case Options.String => string(name); this
   239       case Options.Unknown => this
   240     }
   241   }
   242 
   243   def declare(name: String, typ_name: String, value: String, description: String = ""): Options =
   244   {
   245     options.get(name) match {
   246       case Some(_) => error("Duplicate declaration of option " + quote(name))
   247       case None =>
   248         val typ =
   249           typ_name match {
   250             case "bool" => Options.Bool
   251             case "int" => Options.Int
   252             case "real" => Options.Real
   253             case "string" => Options.String
   254             case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
   255           }
   256         val opt = Options.Opt(name, typ, value, value, description, section)
   257         (new Options(options + (name -> opt), section)).check_value(name)
   258     }
   259   }
   260 
   261   def add_permissive(name: String, value: String): Options =
   262   {
   263     if (options.isDefinedAt(name)) this + (name, value)
   264     else
   265       new Options(
   266         options + (name -> Options.Opt(name, Options.Unknown, value, value, "", "")), section)
   267   }
   268 
   269   def + (name: String, value: String): Options =
   270   {
   271     val opt = check_name(name)
   272     (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name)
   273   }
   274 
   275   def + (name: String, opt_value: Option[String]): Options =
   276   {
   277     val opt = check_name(name)
   278     opt_value match {
   279       case Some(value) => this + (name, value)
   280       case None if opt.typ == Options.Bool => this + (name, "true")
   281       case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
   282     }
   283   }
   284 
   285   def + (str: String): Options =
   286   {
   287     str.indexOf('=') match {
   288       case -1 => this + (str, None)
   289       case i => this + (str.substring(0, i), str.substring(i + 1))
   290     }
   291   }
   292 
   293   def ++ (specs: List[Options.Spec]): Options =
   294     (this /: specs)({ case (x, (y, z)) => x + (y, z) })
   295 
   296 
   297   /* sections */
   298 
   299   def set_section(new_section: String): Options =
   300     new Options(options, new_section)
   301 
   302   def sections: List[(String, List[Options.Opt])] =
   303     options.groupBy(_._2.section).toList.map({ case (a, opts) => (a, opts.toList.map(_._2)) })
   304 
   305 
   306   /* encode */
   307 
   308   def encode: XML.Body =
   309   {
   310     val opts =
   311       for ((name, opt) <- options.toList; if !opt.unknown)
   312         yield (name, opt.typ.print, opt.value)
   313 
   314     import XML.Encode.{string => str, _}
   315     list(triple(str, str, str))(opts)
   316   }
   317 
   318 
   319   /* user preferences */
   320 
   321   def load_prefs(): Options =
   322     if (Options.PREFS.is_file)
   323       Options.Parser.parse_file(
   324         Options.prefs_syntax, Options.Parser.prefs_entry, this, Options.PREFS)
   325     else this
   326 
   327   def save_prefs()
   328   {
   329     val defaults = Options.init_defaults()
   330     val changed =
   331       (for {
   332         (name, opt2) <- options.iterator
   333         opt1 = defaults.options.get(name)
   334         if (opt1.isEmpty || opt1.get.value != opt2.value)
   335       } yield (name, opt2.value, if (opt1.isEmpty) "  (* unknown *)" else "")).toList
   336 
   337     val prefs =
   338       changed.sortBy(_._1)
   339         .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
   340 
   341     Options.PREFS.file renameTo Options.PREFS_BACKUP.file
   342     File.write(Options.PREFS,
   343       "(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs)
   344   }
   345 }
   346 
   347 
   348 class Options_Variable
   349 {
   350   // owned by Swing thread
   351   @volatile private var options = Options.empty
   352 
   353   def value: Options = options
   354   def update(new_options: Options)
   355   {
   356     Swing_Thread.require()
   357     options = new_options
   358   }
   359 
   360   def + (name: String, x: String)
   361   {
   362     Swing_Thread.require()
   363     options = options + (name, x)
   364   }
   365 
   366   val bool = new Object
   367   {
   368     def apply(name: String): Boolean = options.bool(name)
   369     def update(name: String, x: Boolean)
   370     {
   371       Swing_Thread.require()
   372       options = options.bool.update(name, x)
   373     }
   374   }
   375 
   376   val int = new Object
   377   {
   378     def apply(name: String): Int = options.int(name)
   379     def update(name: String, x: Int)
   380     {
   381       Swing_Thread.require()
   382       options = options.int.update(name, x)
   383     }
   384   }
   385 
   386   val real = new Object
   387   {
   388     def apply(name: String): Double = options.real(name)
   389     def update(name: String, x: Double)
   390     {
   391       Swing_Thread.require()
   392       options = options.real.update(name, x)
   393     }
   394   }
   395 
   396   val string = new Object
   397   {
   398     def apply(name: String): String = options.string(name)
   399     def update(name: String, x: String)
   400     {
   401       Swing_Thread.require()
   402       options = options.string.update(name, x)
   403     }
   404   }
   405 }
   406