src/Pure/System/options.scala

--- a/src/Pure/System/options.scala	Sat Jul 21 21:16:08 2012 +0200
+++ b/src/Pure/System/options.scala	Sat Jul 21 22:13:50 2012 +0200
@@ -12,19 +12,24 @@
 
 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 */
 
@@ -58,7 +63,7 @@
     }
   }
 
-  val OPTIONS = Path.explode("etc/options")
+  private val OPTIONS = Path.explode("etc/options")
 
   def init(): Options =
   {
@@ -194,6 +199,9 @@
     }
   }
 
+  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 {