prefer general Properties.Value.Boolean;

--- a/src/Pure/General/properties.scala	Wed Jul 18 20:59:02 2012 +0200
+++ b/src/Pure/General/properties.scala	Thu Jul 19 11:47:49 2012 +0200
@@ -14,6 +14,17 @@
 
   object Value
   {
+    object Boolean
+    {
+      def apply(x: scala.Boolean): java.lang.String = x.toString
+      def unapply(s: java.lang.String): Option[scala.Boolean] =
+        s match {
+          case "true" => Some(true)
+          case "false" => Some(false)
+          case _ => None
+        }
+    }
+
     object Int
     {
       def apply(x: scala.Int): java.lang.String = x.toString
@@ -52,6 +63,16 @@
       props.find(_._1 == name).map(_._2)
   }
 
+  class Boolean(val name: java.lang.String)
+  {
+    def apply(value: scala.Boolean): T = List((name, Value.Boolean(value)))
+    def unapply(props: T): Option[scala.Boolean] =
+      props.find(_._1 == name) match {
+        case None => None
+        case Some((_, value)) => Value.Boolean.unapply(value)
+      }
+  }
+
   class Int(val name: java.lang.String)
   {
     def apply(value: scala.Int): T = List((name, Value.Int(value)))

--- a/src/Pure/System/build.scala	Wed Jul 18 20:59:02 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Jul 19 11:47:49 2012 +0200
@@ -162,16 +162,6 @@
 
   /** command line entry point **/
 
-  private object Bool
-  {
-    def unapply(s: String): Option[Boolean] =
-      s match {
-        case "true" => Some(true)
-        case "false" => Some(false)
-        case _ => None
-      }
-  }
-
   private object Chunks
   {
     private def chunks(list: List[String]): List[List[String]] =
@@ -189,7 +179,10 @@
     val rc =
       try {
         args.toList match {
-          case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) ::
+          case
+            Properties.Value.Boolean(all_sessions) ::
+            Properties.Value.Boolean(build_images) ::
+            Properties.Value.Boolean(list_only) ::
             Chunks(more_dirs, options, sessions) =>
               build(all_sessions, build_images, list_only,
                 more_dirs.map(Path.explode), options, sessions)