# HG changeset patch # User wenzelm # Date 1412453468 -7200 # Node ID b31af96b7f5b3a5ec53ab2bc64cf6c35d98c3e60 # Parent 299b82d12d530201bd65ed119294e520dd4f055d tuned output; diff -r 299b82d12d53 -r b31af96b7f5b src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Oct 04 19:26:31 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Oct 04 22:11:08 2014 +0200 @@ -221,8 +221,12 @@ { override def supportsCompletion = false - private class Asset(label: String, start: Text.Offset, stop: Text.Offset) extends - Isabelle_Sidekick.Asset(label, start, stop) { override def getShortString: String = _name } + private class Asset( + label: String, label_html: String, start: Text.Offset, stop: Text.Offset, source: String) + extends Isabelle_Sidekick.Asset(label, start, stop) { + override def getShortString: String = label_html + override def getLongString: String = source + } def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = { @@ -231,15 +235,17 @@ try { var offset = 0 for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { - val n = chunk.source.size - val label = - ((if (chunk.kind == "") Nil else List(chunk.kind)) ::: - (if (chunk.name == "") Nil else List(chunk.name))).mkString(" ") - if (label != "") { - val asset = new Isabelle_Sidekick.Asset(label, offset, offset + n) + val kind = chunk.kind + val name = chunk.name + val source = chunk.source + if (kind != "") { + val label = kind + (if (name == "") "" else " " + name) + val label_html = + "" + kind + "" + (if (name == "") "" else " " + name) + "" + val asset = new Asset(label, label_html, offset, offset + source.size, source) data.root.add(new DefaultMutableTreeNode(asset)) } - offset += n + offset += source.size } data }