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