# HG changeset patch # User wenzelm # Date 1452373222 -3600 # Node ID 16de2a9b5b3d7acc809bc31880f7c34373a161f3 # Parent 092046740f17f4c9ff007c46f011e04af7e81e9e tuned -- according to ML version; diff -r 092046740f17 -r 16de2a9b5b3d src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Sat Jan 09 20:56:00 2016 +0100 +++ b/src/Pure/GUI/gui.scala Sat Jan 09 22:00:22 2016 +0100 @@ -166,7 +166,7 @@ def tooltip_lines(text: String): String = if (text == null || text == "") null - else "" + HTML.encode(text) + "" + else "" + HTML.output(text) + "" /* icon */ 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 */ diff -r 092046740f17 -r 16de2a9b5b3d src/Tools/jEdit/src/bibtex_jedit.scala --- a/src/Tools/jEdit/src/bibtex_jedit.scala Sat Jan 09 20:56:00 2016 +0100 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala Sat Jan 09 22:00:22 2016 +0100 @@ -254,8 +254,8 @@ if (kind != "") { val label = kind + (if (name == "") "" else " " + name) val label_html = - "" + HTML.encode(kind) + "" + - (if (name == "") "" else " " + HTML.encode(name)) + "" + "" + HTML.output(kind) + "" + + (if (name == "") "" else " " + HTML.output(name)) + "" val range = Text.Range(offset, offset + source.length) val asset = new Asset(label, label_html, range, source) data.root.add(new DefaultMutableTreeNode(asset)) diff -r 092046740f17 -r 16de2a9b5b3d src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Sat Jan 09 20:56:00 2016 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Sat Jan 09 22:00:22 2016 +0100 @@ -35,8 +35,8 @@ private val html = item.description match { case a :: bs => - "" + HTML.encode(a) + "" + - HTML.encode(bs.map(" " + _).mkString) + "" + "" + HTML.output(a) + "" + + HTML.output(bs.map(" " + _).mkString) + "" case Nil => "" } override def toString: String = html diff -r 092046740f17 -r 16de2a9b5b3d src/Tools/jEdit/src/documentation_dockable.scala --- a/src/Tools/jEdit/src/documentation_dockable.scala Sat Jan 09 20:56:00 2016 +0100 +++ b/src/Tools/jEdit/src/documentation_dockable.scala Sat Jan 09 22:00:22 2016 +0100 @@ -24,7 +24,7 @@ private case class Documentation(name: String, title: String, path: Path) { override def toString: String = - "" + HTML.encode(name) + ": " + HTML.encode(title) + "" + "" + HTML.output(name) + ": " + HTML.output(title) + "" } private case class Text_File(name: String, path: Path) diff -r 092046740f17 -r 16de2a9b5b3d src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Jan 09 20:56:00 2016 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Jan 09 22:00:22 2016 +0100 @@ -44,10 +44,10 @@ val s = _name.indexOf(keyword) match { case i if i >= 0 && n > 0 => - HTML.encode(_name.substring(0, i)) + - "" + HTML.encode(keyword) + "" + - HTML.encode(_name.substring(i + n)) - case _ => HTML.encode(_name) + HTML.output(_name.substring(0, i)) + + "" + HTML.output(keyword) + "" + + HTML.output(_name.substring(i + n)) + case _ => HTML.output(_name) } "" + s + "" }