# HG changeset patch
# User wenzelm
# Date 1612022773 -3600
# Node ID 8a17c7bf530af722129d4b7e179edc4753fc4db4
# Parent  b80029a40ccf0fd5eee5f40d0ea78548fe8cb125
tuned signature;

diff -r b80029a40ccf -r 8a17c7bf530a src/Pure/PIDE/xml.scala
--- 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 ++= "&lt;"
@@ -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
diff -r b80029a40ccf -r 8a17c7bf530a src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat Jan 30 13:46:40 2021 +0100
+++ b/src/Pure/Thy/html.scala	Sat Jan 30 17:06:13 2021 +0100
@@ -26,7 +26,7 @@
 
   def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
 
-  def output_char_permissive(c: Char, s: StringBuilder)
+  def output_char_permissive(s: StringBuilder, c: Char)
   {
     c match {
       case '<' => s ++= "&lt;"
@@ -36,11 +36,11 @@
     }
   }
 
-  def output(text: String, s: StringBuilder, hidden: Boolean, permissive: Boolean)
+  def output(s: StringBuilder, text: String, hidden: Boolean, permissive: Boolean)
   {
     def output_char(c: Char): Unit =
-      if (permissive) output_char_permissive(c, s)
-      else XML.output_char(c, s)
+      if (permissive) output_char_permissive(s, c)
+      else XML.output_char(s, c)
 
     def output_string(str: String): Unit =
       str.iterator.foreach(output_char)
@@ -88,7 +88,7 @@
   }
 
   def output(text: String): String =
-    Library.make_string(output(text, _, hidden = false, permissive = true))
+    Library.make_string(output(_, text, hidden = false, permissive = true))
 
 
   /* output XML as HTML */
@@ -97,7 +97,7 @@
     Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
       "ul", "ol", "dl", "li", "dt", "dd")
 
-  def output(body: XML.Body, s: StringBuilder, hidden: Boolean, structural: Boolean)
+  def output(s: StringBuilder, body: XML.Body, hidden: Boolean, structural: Boolean)
   {
     def elem(markup: Markup)
     {
@@ -107,7 +107,7 @@
         s ++= a
         s += '='
         s += '"'
-        output(b, s, hidden = hidden, permissive = false)
+        output(s, b, hidden = hidden, permissive = false)
         s += '"'
       }
     }
@@ -122,13 +122,13 @@
           s ++= "</"; s ++= markup.name; s += '>'
           if (structural && structural_elements(markup.name)) s += '\n'
         case XML.Text(txt) =>
-          output(txt, s, hidden = hidden, permissive = true)
+          output(s, txt, hidden = hidden, permissive = true)
       }
     body.foreach(tree)
   }
 
   def output(body: XML.Body, hidden: Boolean, structural: Boolean): String =
-    Library.make_string(output(body, _, hidden, structural))
+    Library.make_string(output(_, body, hidden, structural))
 
   def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String =
     output(List(tree), hidden, structural)