--- 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"
--- 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 {
--- /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
+ }
+ }
+}
--- 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