diff -r 3f989067f87d -r 41a1210519fd src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Thu May 06 15:04:37 2010 +0200
+++ b/src/Pure/General/markup.scala	Thu May 06 16:27:47 2010 +0200
@@ -9,6 +9,24 @@
 
 object Markup
 {
+  /* property values */
+
+  def get_string(name: String, props: List[(String, String)]): Option[String] =
+    props.find(p => p._1 == name).map(_._2)
+
+  def parse_int(s: String): Option[Int] =
+    try { Some(Integer.parseInt(s)) }
+    catch { case _: NumberFormatException => None }
+
+  def get_int(name: String, props: List[(String, String)]): Option[Int] =
+  {
+    get_string(name, props) match {
+      case None => None
+      case Some(value) => parse_int(value)
+    }
+  }
+
+
   /* name */
 
   val NAME = "name"
@@ -40,6 +58,15 @@
   val LOCATION = "location"
 
 
+  /* pretty printing */
+
+  val INDENT = "indent"
+  val BLOCK = "block"
+  val WIDTH = "width"
+  val BREAK = "break"
+  val FBREAK = "fbreak"
+
+
   /* hidden text */
 
   val HIDDEN = "hidden"