1.1 --- a/src/Pure/System/options.scala	Sat Jul 21 21:16:08 2012 +0200
     1.2 +++ b/src/Pure/System/options.scala	Sat Jul 21 22:13:50 2012 +0200
     1.3 @@ -12,19 +12,24 @@
     1.4  
     1.5  object Options
     1.6  {
     1.7 -  abstract class Type
     1.8 +  type Spec = (String, Option[String])
     1.9 +
    1.10 +  val empty: Options = new Options()
    1.11 +
    1.12 +
    1.13 +  /* representation */
    1.14 +
    1.15 +  sealed abstract class Type
    1.16    {
    1.17      def print: String = toString.toLowerCase
    1.18    }
    1.19 -  case object Bool extends Type
    1.20 -  case object Int extends Type
    1.21 -  case object Real extends Type
    1.22 -  case object String extends Type
    1.23 +  private case object Bool extends Type
    1.24 +  private case object Int extends Type
    1.25 +  private case object Real extends Type
    1.26 +  private case object String extends Type
    1.27  
    1.28    case class Opt(typ: Type, value: String, description: String)
    1.29  
    1.30 -  val empty: Options = new Options()
    1.31 -
    1.32  
    1.33    /* parsing */
    1.34  
    1.35 @@ -58,7 +63,7 @@
    1.36      }
    1.37    }
    1.38  
    1.39 -  val OPTIONS = Path.explode("etc/options")
    1.40 +  private val OPTIONS = Path.explode("etc/options")
    1.41  
    1.42    def init(): Options =
    1.43    {
    1.44 @@ -194,6 +199,9 @@
    1.45      }
    1.46    }
    1.47  
    1.48 +  def ++ (specs: List[Options.Spec]): Options =
    1.49 +    (this /: specs)({ case (x, (y, z)) => x.define(y, z) })
    1.50 +
    1.51    def define_simple(str: String): Options =
    1.52    {
    1.53      str.indexOf('=') match {