support for XML name spaces;

--- a/src/Pure/PIDE/xml.scala	Thu Feb 14 14:44:41 2019 +0100
+++ b/src/Pure/PIDE/xml.scala	Thu Feb 14 15:44:02 2019 +0100
@@ -35,6 +35,23 @@
   def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
 
 
+  /* name space */
+
+  object Namespace
+  {
+    def apply(prefix: String, target: String): Namespace =
+      new Namespace(prefix, target)
+  }
+
+  final class Namespace private(prefix: String, target: String)
+  {
+    def apply(name: String): String = prefix + ":" + name
+    val attribute: XML.Attribute = ("xmlns:" + prefix, target)
+
+    override def toString: String = attribute.toString
+  }
+
+
   /* wrapped elements */
 
   val XML_ELEM = "xml_elem"