# HG changeset patch
# User wenzelm
# Date 1261135730 -3600
# Node ID ae92efb4878478a0a95d3803fcd990669c2d5b58
# Parent  ee9f87e11400d2cb4ac50a0858a7ffb0c2c2a3f5
markup bad YXML as malformed;
removed unused XML.document;
removed unused markup;

diff -r ee9f87e11400 -r ae92efb48784 src/Pure/General/markup.scala
--- 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"
 }
diff -r ee9f87e11400 -r ae92efb48784 src/Pure/General/xml.scala
--- 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
-  }
 }
diff -r ee9f87e11400 -r ae92efb48784 src/Pure/General/yxml.scala
--- 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] =