# 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))