--- a/src/Pure/PIDE/xml.scala Wed May 31 21:48:32 2017 +0200
+++ b/src/Pure/PIDE/xml.scala Thu Jun 01 11:57:04 2017 +0200
@@ -93,23 +93,29 @@
/** string representation **/
+ def output_char(c: Char, s: StringBuilder)
+ {
+ c match {
+ case '<' => s ++= "<"
+ case '>' => s ++= ">"
+ case '&' => s ++= "&"
+ case '"' => s ++= """
+ case '\'' => s ++= "'"
+ case _ => s += c
+ }
+ }
+
+ def output_string(str: String, s: StringBuilder)
+ {
+ if (str == null) s ++= str
+ else str.iterator.foreach(c => output_char(c, s))
+ }
+
def string_of_body(body: Body): String =
{
val s = new StringBuilder
- def text(txt: String) {
- if (txt == null) s ++= txt
- else {
- for (c <- txt.iterator) c match {
- case '<' => s ++= "<"
- case '>' => s ++= ">"
- case '&' => s ++= "&"
- case '"' => s ++= """
- case '\'' => s ++= "'"
- case _ => s += c
- }
- }
- }
+ def text(txt: String) { output_string(txt, s) }
def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
def tree(t: Tree): Unit =
--- a/src/Pure/Thy/html.scala Wed May 31 21:48:32 2017 +0200
+++ b/src/Pure/Thy/html.scala Thu Jun 01 11:57:04 2017 +0200
@@ -22,17 +22,7 @@
def output(text: String, s: StringBuilder)
{
- def output_char(c: Char) =
- c match {
- case '<' => s ++= "<"
- case '>' => s ++= ">"
- case '&' => s ++= "&"
- case '"' => s ++= """
- case '\'' => s ++= "'"
- case '\n' => s ++= "<br/>"
- case _ => s += c
- }
- def output_chars(str: String) = str.iterator.foreach(output_char(_))
+ def output_string(str: String) = XML.output_string(str, s)
var ctrl = ""
for (sym <- Symbol.iterator(text)) {
@@ -41,16 +31,16 @@
control.get(ctrl) match {
case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
s ++= ("<" + elem + ">")
- output_chars(sym)
+ output_string(sym)
s ++= ("</" + elem + ">")
case _ =>
- output_chars(ctrl)
- output_chars(sym)
+ output_string(ctrl)
+ output_string(sym)
}
ctrl = ""
}
}
- output_chars(ctrl)
+ output_string(ctrl)
}
def output(text: String): String = Library.make_string(output(text, _))