diff -r 092046740f17 -r 16de2a9b5b3d src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Sat Jan 09 20:56:00 2016 +0100 +++ b/src/Pure/Thy/html.scala Sat Jan 09 22:00:22 2016 +0100 @@ -20,11 +20,11 @@ Symbol.bold -> "b", Symbol.bold_decoded -> "b") - def encode(text: String): String = + def output(text: String): String = { val result = new StringBuilder - def encode_char(c: Char) = + def output_char(c: Char) = c match { case '<' => result ++= "<" case '>' => result ++= ">" @@ -34,7 +34,7 @@ case '\n' => result ++= "
" case _ => result += c } - def encode_chars(s: String) = s.iterator.foreach(encode_char(_)) + def output_chars(s: String) = s.iterator.foreach(output_char(_)) var ctrl = "" for (sym <- Symbol.iterator(text)) { @@ -43,16 +43,16 @@ control.get(ctrl) match { case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" => result ++= ("<" + elem + ">") - encode_chars(sym) + output_chars(sym) result ++= ("") case _ => - encode_chars(ctrl) - encode_chars(sym) + output_chars(ctrl) + output_chars(sym) } ctrl = "" } } - encode_chars(ctrl) + output_chars(ctrl) result.toString } @@ -60,8 +60,6 @@ /* document */ - val end_document = "\n\n\n\n" - def begin_document(title: String): String = "\n" + "\n" + "\n" + "\n" + - "" + encode(title) + "\n" + + "" + output(title + " (" + Distribution.version + ")") + "\n" + "\n" + "\n" + "\n" + "\n" + "

" + - "

" + encode(title) + "

\n" + "

" + output(title) + "

\n" + + val end_document = "\n

\n\n\n" /* common markup elements */