--- a/src/Pure/PIDE/xml.scala Sat Jan 30 13:46:40 2021 +0100
+++ b/src/Pure/PIDE/xml.scala Sat Jan 30 17:06:13 2021 +0100
@@ -128,7 +128,7 @@
val header: String = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n"
- def output_char(c: Char, s: StringBuilder)
+ def output_char(s: StringBuilder, c: Char)
{
c match {
case '<' => s ++= "<"
@@ -140,17 +140,17 @@
}
}
- def output_string(str: String, s: StringBuilder)
+ def output_string(s: StringBuilder, str: String)
{
if (str == null) s ++= str
- else str.iterator.foreach(c => output_char(c, s))
+ else str.iterator.foreach(c => output_char(s, c))
}
def string_of_body(body: Body): String =
{
val s = new StringBuilder
- def text(txt: String) { output_string(txt, s) }
+ def text(txt: String) { output_string(s, txt) }
def elem(markup: Markup)
{
s ++= markup.name