# HG changeset patch
# User wenzelm
# Date 1550155442 -3600
# Node ID a8debe27c36cadf22b46fb26b62125431cd19a5f
# Parent  9efccbad7d425d10cf2bfaccffa8ff87c057b956
support for XML name spaces;

diff -r 9efccbad7d42 -r a8debe27c36c src/Pure/PIDE/xml.scala
--- 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"