# HG changeset patch # User wenzelm # Date 1719518949 -7200 # Node ID 6f4d5d922da712b8af43e3acf25b43a886189943 # Parent 5fe811816fa381b762772c39f5c883b5abcf0ef9 clarified signature: more explicit types; diff -r 5fe811816fa3 -r 6f4d5d922da7 src/Pure/General/html.scala --- a/src/Pure/General/html.scala Thu Jun 27 00:11:53 2024 +0200 +++ b/src/Pure/General/html.scala Thu Jun 27 22:09:09 2024 +0200 @@ -170,8 +170,10 @@ hidden: Boolean, permissive: Boolean ): Unit = { + val xml_output = new XML.Output(s) + def output_string(str: String): Unit = - XML.output_string(s, str, permissive = permissive) + xml_output.string(str, permissive = permissive) def output_hidden(body: => Unit): Unit = if (hidden) { s ++= ""; body; s ++= "" } @@ -181,11 +183,11 @@ control_block_begin.get(sym) match { case Some(op) if control_blocks => output_hidden(output_string(sym)) - XML.output_elem(s, Markup(op.name, Nil)) + xml_output.elem(Markup(op.name, Nil)) case _ => control_block_end.get(sym) match { case Some(op) if control_blocks => - XML.output_elem_end(s, op.name) + xml_output.end_elem(op.name) output_hidden(output_string(sym)) case _ => if (hidden && Symbol.is_control_encoded(sym)) { @@ -207,9 +209,9 @@ control.get(ctrl) match { case Some(op) if Symbol.is_controllable(sym) => output_hidden(output_symbol(ctrl)) - XML.output_elem(s, Markup(op.name, Nil)) + xml_output.elem(Markup(op.name, Nil)) output_symbol(sym) - XML.output_elem_end(s, op.name) + xml_output.end_elem(op.name) case _ => output_symbol(ctrl) output_symbol(sym) @@ -234,18 +236,20 @@ "ul", "ol", "dl", "li", "dt", "dd") def output(s: StringBuilder, xml: XML.Body, hidden: Boolean, structural: Boolean): Unit = { + val xml_output = new XML.Output(s) + def output_body(body: XML.Body): Unit = { val control_blocks = check_control_blocks(body) body foreach { case XML.Elem(markup, Nil) => - XML.output_elem(s, markup, end = true) + xml_output.elem(markup, end = true) case XML.Elem(Markup(Markup.RAW_HTML, _), body) => XML.traverse_text(body)(()) { case (_, raw) => s.append(raw) } case XML.Elem(markup, ts) => if (structural && structural_elements(markup.name)) s += '\n' - XML.output_elem(s, markup) + xml_output.elem(markup) output_body(ts) - XML.output_elem_end(s, markup.name) + xml_output.end_elem(markup.name) if (structural && structural_elements(markup.name)) s += '\n' case XML.Text(txt) => output(s, txt, control_blocks = control_blocks, hidden = hidden, permissive = true) diff -r 5fe811816fa3 -r 6f4d5d922da7 src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Thu Jun 27 00:11:53 2024 +0200 +++ b/src/Pure/PIDE/xml.scala Thu Jun 27 22:09:09 2024 +0200 @@ -46,6 +46,20 @@ 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 + def end_elem(name: String): Unit + + def tree(t: Tree): Unit = + t match { + case Text(s) => text(s) + case Elem(markup, Nil) => elem(markup, end = true) + case Elem(markup, ts) => elem(markup); trees(ts); end_elem(markup.name) + } + def trees(ts: Iterable[Tree]): Unit = ts.foreach(tree) + } + /* name space */ @@ -125,66 +139,61 @@ val header: String = "\n" - def output_char(s: StringBuilder, c: Char, permissive: Boolean = false): Unit = { - c match { - case '<' => s ++= "<" - case '>' => s ++= ">" - case '&' => s ++= "&" - case '"' if !permissive => s ++= """ - case '\'' if !permissive => s ++= "'" - case _ => s += c + class Output(builder: StringBuilder) extends Traversal { + def string(str: String, permissive: Boolean = false): Unit = { + if (str == null) { builder ++= str } + else { + for (c <- str) { + c match { + case '<' => builder ++= "<" + case '>' => builder ++= ">" + case '&' => builder ++= "&" + case '"' if !permissive => builder ++= """ + case '\'' if !permissive => builder ++= "'" + case _ => builder += c + } + } + } } - } + + override def text(str: String): Unit = string(str) - def output_string(s: StringBuilder, str: String, permissive: Boolean = false): Unit = { - if (str == null) s ++= str - else str.iterator.foreach(output_char(s, _, permissive = permissive)) + override def elem(markup: Markup, end: Boolean = false): Unit = { + builder += '<' + builder ++= markup.name + for ((a, b) <- markup.properties) { + builder += ' ' + builder ++= a + builder += '=' + builder += '"' + string(b) + builder += '"' + } + if (end) builder += '/' + builder += '>' + } + + def end_elem(name: String): Unit = { + builder += '<' + builder += '/' + builder ++= name + builder += '>' + } + + def result(ts: Iterable[Tree]): String = { trees(ts); builder.toString } + def result(t: Tree): String = { tree(t); builder.toString } } - def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false): Unit = { - s += '<' - s ++= markup.name - for ((a, b) <- markup.properties) { - s += ' ' - s ++= a - s += '=' - s += '"' - output_string(s, b) - s += '"' - } - if (end) s += '/' - s += '>' - } - - def output_elem_end(s: StringBuilder, name: String): Unit = { - s += '<' - s += '/' - s ++= name - s += '>' - } - - def string_of_body(body: Body): String = { - val s = new StringBuilder - - def tree(t: Tree): Unit = - t match { - case XML.Elem(markup, Nil) => - output_elem(s, markup, end = true) - case XML.Elem(markup, ts) => - output_elem(s, markup) - ts.foreach(tree) - output_elem_end(s, markup.name) - case XML.Text(txt) => output_string(s, txt) - } - body.foreach(tree) - s.toString - } + def string_of_body(body: Body): String = + if (body.isEmpty) "" + else new Output(new StringBuilder).result(body) def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree)) def text(s: String): String = string_of_tree(XML.Text(s)) + /** cache **/ object Cache {