markup bad YXML as malformed;
removed unused XML.document;
removed unused markup;
--- a/src/Pure/General/markup.scala Fri Dec 18 12:10:52 2009 +0100
+++ b/src/Pure/General/markup.scala Fri Dec 18 12:28:50 2009 +0100
@@ -182,9 +182,7 @@
val READY = "ready"
- /* content */
+ /* system data */
- val ROOT = "root"
- val BAD = "bad"
val DATA = "data"
}
--- a/src/Pure/General/xml.scala Fri Dec 18 12:10:52 2009 +0100
+++ b/src/Pure/General/xml.scala Fri Dec 18 12:28:50 2009 +0100
@@ -171,21 +171,4 @@
}
DOM(tree)
}
-
- def document(tree: Tree, styles: String*): Document =
- {
- val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument
- doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\""))
-
- for (style <- styles) {
- doc.appendChild(doc.createProcessingInstruction("xml-stylesheet",
- "href=\"" + style + "\" type=\"text/css\""))
- }
- val root_elem = tree match {
- case Elem(_, _, _) => document_node(doc, tree)
- case Text(_) => document_node(doc, (Elem(Markup.ROOT, Nil, List(tree))))
- }
- doc.appendChild(root_elem)
- doc
- }
}
--- a/src/Pure/General/yxml.scala Fri Dec 18 12:10:52 2009 +0100
+++ b/src/Pure/General/yxml.scala Fri Dec 18 12:28:50 2009 +0100
@@ -171,7 +171,7 @@
/* failsafe parsing */
private def markup_failsafe(source: CharSequence) =
- XML.Elem (Markup.BAD, Nil,
+ XML.Elem (Markup.MALFORMED, Nil,
List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
def parse_body_failsafe(source: CharSequence): List[XML.Tree] =