src/Pure/General/properties.scala

--- 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)))