# HG changeset patch
# User wenzelm
# Date 1719524179 -7200
# Node ID 6f1c8084f67239ad6b2a3ff8460682b4e44ec512
# Parent  48776d779d947829ab159819d2e361a5fac27015
tuned module structure;

diff -r 48776d779d94 -r 6f1c8084f672 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Thu Jun 27 23:32:24 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Jun 27 23:36:19 2024 +0200
@@ -41,18 +41,6 @@
     override def hashCode(): Int = hash
   }
 
-  def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil)
-  def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
-  def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
-
-  val no_text: Text = Text("")
-  val newline: Text = Text("\n")
-
-  def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s))
-
-  def enclose(bg: String, en:String, body: Body): Body =
-    string(bg) ::: body ::: string(en)
-
   trait Traversal {
     def text(s: String): Unit
     def elem(markup: Markup, end: Boolean = false): Unit
@@ -74,6 +62,18 @@
     }
   }
 
+  def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil)
+  def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
+  def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
+
+  val no_text: Text = Text("")
+  val newline: Text = Text("\n")
+
+  def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s))
+
+  def enclose(bg: String, en:String, body: Body): Body =
+    string(bg) ::: body ::: string(en)
+
 
   /* name space */