src/Pure/General/markup.scala

 package isabelle
 
 
 object Markup
 {
-  /* integers */
+  /* plain values */
 
   object Int {
     def apply(i: scala.Int): String = i.toString
     def unapply(s: String): Option[scala.Int] =
       try { Some(Integer.parseInt(s)) }

       try { Some(java.lang.Long.parseLong(s)) }
       catch { case _: NumberFormatException => None }
   }
 
 
-  /* property values */
-
-  def get_string(name: String, props: List[(String, String)]): Option[String] =
-    props.find(p => p._1 == name).map(_._2)
-
-  def get_long(name: String, props: List[(String, String)]): Option[scala.Long] =
+  /* named properties */
+
+  class Property(val name: String)
   {
-    get_string(name, props) match {
-      case None => None
-      case Some(Long(i)) => Some(i)
-    }
-  }
-
-  def get_int(name: String, props: List[(String, String)]): Option[scala.Int] =
+    def apply(value: String): List[(String, String)] = List((name, value))
+    def unapply(props: List[(String, String)]): Option[String] =
+      props.find(_._1 == name).map(_._2)
+  }
+
+  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)
+      }
   }
 
 
   /* empty */