added Markup.Double, Markup.Double_Property;
tuned;

--- a/src/Pure/General/markup.scala	Sat Nov 06 16:31:35 2010 +0100
+++ b/src/Pure/General/markup.scala	Sat Nov 06 16:53:07 2010 +0100
@@ -11,20 +11,30 @@
 {
   /* plain values */
 
-  object Int {
-    def apply(i: scala.Int): String = i.toString
+  object Int
+  {
+    def apply(x: scala.Int): String = x.toString
     def unapply(s: String): Option[scala.Int] =
       try { Some(Integer.parseInt(s)) }
       catch { case _: NumberFormatException => None }
   }
 
-  object Long {
-    def apply(i: scala.Long): String = i.toString
+  object Long
+  {
+    def apply(x: scala.Long): String = x.toString
     def unapply(s: String): Option[scala.Long] =
       try { Some(java.lang.Long.parseLong(s)) }
       catch { case _: NumberFormatException => None }
   }
 
+  object Double
+  {
+    def apply(x: scala.Double): String = x.toString
+    def unapply(s: String): Option[scala.Double] =
+      try { Some(java.lang.Double.parseDouble(s)) }
+      catch { case _: NumberFormatException => None }
+  }
+
 
   /* named properties */
 
@@ -55,6 +65,16 @@
       }
   }
 
+  class Double_Property(name: String)
+  {
+    def apply(value: scala.Double): List[(String, String)] = List((name, Double(value)))
+    def unapply(props: List[(String, String)]): Option[Double] =
+      props.find(_._1 == name) match {
+        case None => None
+        case Some((_, value)) => Double.unapply(value)
+      }
+  }
+
 
   /* empty */