tuned module structure;
authorwenzelm
Thu, 27 Jun 2024 23:36:19 +0200
changeset 80434 6f1c8084f672
parent 80433 48776d779d94
child 80435 de2ea807edd2
tuned module structure;
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 */