# HG changeset patch # User wenzelm # Date 1230585604 -3600 # Node ID 0c4effb7351868bdf6975de4c1071b67b4d14b64 # Parent 2454172eddae2b8a87a6c29d1cf8c8f89be70ef4 override toString method; diff -r 2454172eddae -r 0c4effb73518 src/Pure/General/xml.scala --- a/src/Pure/General/xml.scala Mon Dec 29 20:06:31 2008 +0100 +++ b/src/Pure/General/xml.scala Mon Dec 29 22:20:04 2008 +0100 @@ -10,14 +10,53 @@ import javax.xml.parsers.DocumentBuilderFactory -object XML { +object XML +{ /* datatype representation */ type Attributes = List[(String, String)] abstract class Tree - case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree - case class Text(content: String) extends Tree + case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree { + override def toString = append_tree(this, new StringBuilder).toString + } + case class Text(content: String) extends Tree { + override def toString = append_tree(this, new StringBuilder).toString + } + + + /* string representation */ + + private def append_text(text: String, s: StringBuilder) { + for (c <- text.elements) c match { + case '<' => s.append("<") + case '>' => s.append(">") + case '&' => s.append("&") + case '"' => s.append(""") + case '\'' => s.append("'") + case _ => s.append(c) + } + } + + private def append_elem(name: String, atts: Attributes, s: StringBuilder) { + s.append(name) + for ((a, x) <- atts) { + s.append(" "); s.append(a); s.append("=\""); append_text(x, s); s.append("\"") + } + } + + private def append_tree(tree: Tree, s: StringBuilder): StringBuilder = { + tree match { + case Elem(name, atts, Nil) => + s.append("<"); append_elem(name, atts, s); s.append("/>") + case Elem(name, atts, ts) => + s.append("<"); append_elem(name, atts, s); s.append(">") + for (t <- ts) append_tree(t, s) + s.append("") + case Text(text) => append_text(text, s) + } + s + } /* iterate over content */