src/Pure/System/options.scala

 import java.io.{File => JFile}
 
 
 object Options
 {
-  abstract class Type
+  type Spec = (String, Option[String])
+
+  val empty: Options = new Options()
+
+
+  /* representation */
+
+  sealed abstract class Type
   {
     def print: String = toString.toLowerCase
   }
-  case object Bool extends Type
-  case object Int extends Type
-  case object Real extends Type
-  case object String extends Type
+  private case object Bool extends Type
+  private case object Int extends Type
+  private case object Real extends Type
+  private case object String extends Type
 
   case class Opt(typ: Type, value: String, description: String)
-
-  val empty: Options = new Options()
 
 
   /* parsing */
 
   private object Parser extends Parse.Parser

         case bad => error(bad.toString)
       }
     }
   }
 
-  val OPTIONS = Path.explode("etc/options")
+  private val OPTIONS = Path.explode("etc/options")
 
   def init(): Options =
   {
     var options = empty
     for {

       case None if opt.typ == Options.Bool => define(name, "true")
       case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
     }
   }
 
+  def ++ (specs: List[Options.Spec]): Options =
+    (this /: specs)({ case (x, (y, z)) => x.define(y, z) })
+
   def define_simple(str: String): Options =
   {
     str.indexOf('=') match {
       case -1 => define(str, None)
       case i => define(str.substring(0, i), str.substring(i + 1))