diff -r ca8b14fa0d0d -r ba31936497c2 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Wed Aug 25 21:31:22 2010 +0200
+++ b/src/Pure/General/markup.scala	Wed Aug 25 22:37:53 2010 +0200
@@ -9,7 +9,7 @@
 
 object Markup
 {
-  /* integers */
+  /* plain values */
 
   object Int {
     def apply(i: scala.Int): String = i.toString
@@ -26,25 +26,33 @@
   }
 
 
-  /* property values */
-
-  def get_string(name: String, props: List[(String, String)]): Option[String] =
-    props.find(p => p._1 == name).map(_._2)
+  /* named properties */
 
-  def get_long(name: String, props: List[(String, String)]): Option[scala.Long] =
+  class Property(val name: String)
   {
-    get_string(name, props) match {
-      case None => None
-      case Some(Long(i)) => Some(i)
-    }
+    def apply(value: String): List[(String, String)] = List((name, value))
+    def unapply(props: List[(String, String)]): Option[String] =
+      props.find(_._1 == name).map(_._2)
   }
 
-  def get_int(name: String, props: List[(String, String)]): Option[scala.Int] =
+  class Int_Property(name: String)
   {
-    get_string(name, props) match {
-      case None => None
-      case Some(Int(i)) => Some(i)
-    }
+    def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
+    def unapply(props: List[(String, String)]): Option[Int] =
+      props.find(_._1 == name) match {
+        case None => None
+        case Some((_, value)) => Int.unapply(value)
+      }
+  }
+
+  class Long_Property(name: String)
+  {
+    def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
+    def unapply(props: List[(String, String)]): Option[Long] =
+      props.find(_._1 == name) match {
+        case None => None
+        case Some((_, value)) => Long.unapply(value)
+      }
   }