--- 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 =
- "<html><b>" + kind + "</b>" + (if (name == "") "" else " " + name) + "</html>"
+ "<html><b>" + HTML.encode(kind) + "</b>" +
+ (if (name == "") "" else " " + HTML.encode(name)) + "</html>"
val range = Text.Range(offset, offset + source.size)
val asset = new Asset(label, label_html, range, source)
data.root.add(new DefaultMutableTreeNode(asset))