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