src/Pure/General/pretty.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/pretty.scala	Thu May 06 16:27:47 2010 +0200
@@ -0,0 +1,50 @@
+/*  Title:      Pure/General/pretty.scala
+    Author:     Makarius
+
+Symbolic pretty printing.
+*/
+
+package isabelle
+
+
+object Pretty
+{
+  object Block
+  {
+    def apply(indent: Int, body: List[XML.Tree]): XML.Tree =
+      XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent.toString)), body)
+
+    def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
+      tree match {
+        case XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent)), body) =>
+          Markup.parse_int(indent) match {
+            case Some(i) => Some((i, body))
+            case None => None
+          }
+        case _ => None
+      }
+  }
+
+  object Break
+  {
+    def apply(width: Int): XML.Tree =
+      XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)), List(XML.Text(" " * width)))
+
+    def unapply(tree: XML.Tree): Option[Int] =
+      tree match {
+        case XML.Elem(Markup.BREAK, List((Markup.WIDTH, width)), _) => Markup.parse_int(width)
+        case _ => None
+      }
+  }
+
+  object FBreak
+  {
+    def apply(): XML.Tree = XML.Elem(Markup.FBREAK, Nil, List(XML.Text(" ")))
+
+    def unapply(tree: XML.Tree): Boolean =
+      tree match {
+        case XML.Elem(Markup.FBREAK, Nil, _) => true
+        case _ => false
+      }
+  }
+}