# HG changeset patch
# User wenzelm
# Date 1273156067 -7200
# Node ID 41a1210519fdc5c8e5a66a3a1c15c2423968c3e2
# Parent  3f989067f87de5cda42359f516eae1c18625dad1
basic support for symbolic pretty printing;
tuned;

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"
diff -r 3f989067f87d -r 41a1210519fd src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Thu May 06 15:04:37 2010 +0200
+++ b/src/Pure/General/position.scala	Thu May 06 16:27:47 2010 +0200
@@ -11,27 +11,14 @@
 {
   type T = List[(String, String)]
 
-  private def get_string(name: String, pos: T): Option[String] =
-    pos.find(p => p._1 == name).map(_._2)
-
-  private def get_int(name: String, pos: T): Option[Int] =
-  {
-    get_string(name, pos) match {
-      case None => None
-      case Some(value) =>
-        try { Some(Integer.parseInt(value)) }
-        catch { case _: NumberFormatException => None }
-    }
-  }
-
-  def get_line(pos: T): Option[Int] = get_int(Markup.LINE, pos)
-  def get_column(pos: T): Option[Int] = get_int(Markup.COLUMN, pos)
-  def get_offset(pos: T): Option[Int] = get_int(Markup.OFFSET, pos)
-  def get_end_line(pos: T): Option[Int] = get_int(Markup.END_LINE, pos)
-  def get_end_column(pos: T): Option[Int] = get_int(Markup.END_COLUMN, pos)
-  def get_end_offset(pos: T): Option[Int] = get_int(Markup.END_OFFSET, pos)
-  def get_file(pos: T): Option[String] = get_string(Markup.FILE, pos)
-  def get_id(pos: T): Option[String] = get_string(Markup.ID, pos)
+  def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos)
+  def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos)
+  def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos)
+  def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos)
+  def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
+  def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
+  def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
+  def get_id(pos: T): Option[String] = Markup.get_string(Markup.ID, pos)
 
   def get_range(pos: T): Option[(Int, Int)] =
     (get_offset(pos), get_end_offset(pos)) match {
diff -r 3f989067f87d -r 41a1210519fd 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
+      }
+  }
+}
diff -r 3f989067f87d -r 41a1210519fd src/Pure/build-jars
--- a/src/Pure/build-jars	Thu May 06 15:04:37 2010 +0200
+++ b/src/Pure/build-jars	Thu May 06 16:27:47 2010 +0200
@@ -27,6 +27,7 @@
   General/linear_set.scala
   General/markup.scala
   General/position.scala
+  General/pretty.scala
   General/scan.scala
   General/symbol.scala
   General/xml.scala