1.1 --- a/src/Pure/System/options.scala	Sun Aug 19 18:01:25 2012 +0200
     1.2 +++ b/src/Pure/System/options.scala	Sun Aug 19 19:31:45 2012 +0200
     1.3 @@ -27,8 +27,12 @@
     1.4    private case object Int extends Type
     1.5    private case object Real extends Type
     1.6    private case object String extends Type
     1.7 +  private case object Unknown extends Type
     1.8  
     1.9    case class Opt(typ: Type, value: String, description: String)
    1.10 +  {
    1.11 +    def unknown: Boolean = typ == Unknown
    1.12 +  }
    1.13  
    1.14  
    1.15    /* parsing */
    1.16 @@ -60,7 +64,7 @@
    1.17      val prefs_entry: Parser[Options => Options] =
    1.18      {
    1.19        option_name ~ (keyword("=") ~! option_value) ^^
    1.20 -      { case a ~ (_ ~ b) => (options: Options) => options + (a, b) }
    1.21 +      { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) }
    1.22      }
    1.23  
    1.24      def parse_file(syntax: Outer_Syntax, parser: Parser[Options => Options],
    1.25 @@ -123,15 +127,15 @@
    1.26      cat_lines(options.toList.sortBy(_._1).map({ case (name, opt) =>
    1.27        "option " + name + " : " + opt.typ.print + " = " +
    1.28          (if (opt.typ == Options.String) quote(opt.value) else opt.value) +
    1.29 -      "\n  -- " + quote(opt.description) }))
    1.30 +      (if (opt.description == "") "" else "\n  -- " + quote(opt.description)) }))
    1.31  
    1.32  
    1.33    /* check */
    1.34  
    1.35    private def check_name(name: String): Options.Opt =
    1.36      options.get(name) match {
    1.37 -      case Some(opt) => opt
    1.38 -      case None => error("Unknown option " + quote(name))
    1.39 +      case Some(opt) if !opt.unknown => opt
    1.40 +      case _ => error("Unknown option " + quote(name))
    1.41      }
    1.42  
    1.43    private def check_type(name: String, typ: Options.Type): Options.Opt =
    1.44 @@ -202,6 +206,7 @@
    1.45        case Options.Int => int(name); this
    1.46        case Options.Real => real(name); this
    1.47        case Options.String => string(name); this
    1.48 +      case Options.Unknown => this
    1.49      }
    1.50    }
    1.51  
    1.52 @@ -223,6 +228,12 @@
    1.53      }
    1.54    }
    1.55  
    1.56 +  def add_permissive(name: String, value: String): Options =
    1.57 +  {
    1.58 +    if (options.isDefinedAt(name)) this + (name, value)
    1.59 +    else new Options(options + (name -> Options.Opt(Options.Unknown, value, "")))
    1.60 +  }
    1.61 +
    1.62    def + (name: String, value: String): Options =
    1.63    {
    1.64      val opt = check_name(name)
    1.65 @@ -255,9 +266,12 @@
    1.66  
    1.67    def encode: XML.Body =
    1.68    {
    1.69 +    val opts =
    1.70 +      for ((name, opt) <- options.toList; if !opt.unknown)
    1.71 +        yield (name, opt.typ.print, opt.value)
    1.72 +
    1.73      import XML.Encode.{string => str, _}
    1.74 -    list(triple(str, str, str))(
    1.75 -      options.toList.map({ case (name, opt) => (name, opt.typ.print, opt.value) }))
    1.76 +    list(triple(str, str, str))(opts)
    1.77    }
    1.78  
    1.79  
    1.80 @@ -271,16 +285,17 @@
    1.81  
    1.82    def save_prefs()
    1.83    {
    1.84 -    val current_defaults = Options.init_defaults()
    1.85 +    val defaults = Options.init_defaults()
    1.86      val changed =
    1.87        (for {
    1.88 -        (name, opt1) <- current_defaults.options.iterator
    1.89 -        opt2 <- options.get(name)
    1.90 -        if (opt1.value != opt2.value)
    1.91 -      } yield (name, opt2.value)).toList
    1.92 +        (name, opt2) <- options.iterator
    1.93 +        opt1 = defaults.options.get(name)
    1.94 +        if (opt1.isEmpty || opt1.get.value != opt2.value)
    1.95 +      } yield (name, opt2.value, if (opt1.isEmpty) "  (* unknown *)" else "")).toList
    1.96 +
    1.97      val prefs =
    1.98        changed.sortBy(_._1)
    1.99 -        .map({ case (x, y) => x + " = " + Outer_Syntax.quote_string(y) + "\n" }).mkString
   1.100 +        .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
   1.101  
   1.102      Options.PREFS.file renameTo Options.PREFS_BACKUP.file
   1.103      File.write(Options.PREFS,