equal
deleted
inserted
replaced
240 |
240 |
241 true |
241 true |
242 } |
242 } |
243 } |
243 } |
244 |
244 |
245 |
|
246 class Isabelle_Sidekick_Bibtex extends SideKickParser("bibtex") |
|
247 { |
|
248 override def supportsCompletion = false |
|
249 |
|
250 private class Asset( |
|
251 label: String, label_html: String, start: Text.Offset, stop: Text.Offset, source: String) |
|
252 extends Isabelle_Sidekick.Asset(label, start, stop) { |
|
253 override def getShortString: String = label_html |
|
254 override def getLongString: String = source |
|
255 } |
|
256 |
|
257 def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = |
|
258 { |
|
259 val data = Isabelle_Sidekick.root_data(buffer) |
|
260 |
|
261 try { |
|
262 var offset = 0 |
|
263 for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { |
|
264 val kind = chunk.kind |
|
265 val name = chunk.name |
|
266 val source = chunk.source |
|
267 if (kind != "") { |
|
268 val label = kind + (if (name == "") "" else " " + name) |
|
269 val label_html = |
|
270 "<html><b>" + kind + "</b>" + (if (name == "") "" else " " + name) + "</html>" |
|
271 val asset = new Asset(label, label_html, offset, offset + source.size, source) |
|
272 data.root.add(new DefaultMutableTreeNode(asset)) |
|
273 } |
|
274 offset += source.size |
|
275 } |
|
276 data |
|
277 } |
|
278 catch { case ERROR(_) => null } |
|
279 } |
|
280 } |
|
281 |
|