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