# HG changeset patch # User wenzelm # Date 1417268552 -3600 # Node ID f26598b1a0da15f82c1eb1960d7be65b4f911f3d # Parent 67771d267ff2163c39d929bf3d0d72789920ff86 proper HTML.encode; diff -r 67771d267ff2 -r f26598b1a0da src/Tools/jEdit/src/bibtex_jedit.scala --- a/src/Tools/jEdit/src/bibtex_jedit.scala Wed Nov 26 15:59:46 2014 +0100 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala Sat Nov 29 14:42:32 2014 +0100 @@ -250,7 +250,8 @@ if (kind != "") { val label = kind + (if (name == "") "" else " " + name) val label_html = - "" + kind + "" + (if (name == "") "" else " " + name) + "" + "" + HTML.encode(kind) + "" + + (if (name == "") "" else " " + HTML.encode(name)) + "" val range = Text.Range(offset, offset + source.size) val asset = new Asset(label, label_html, range, source) data.root.add(new DefaultMutableTreeNode(asset))