270 |
270 |
271 def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = { |
271 def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = { |
272 val data = Isabelle_Sidekick.root_data(buffer) |
272 val data = Isabelle_Sidekick.root_data(buffer) |
273 |
273 |
274 try { |
274 try { |
|
275 val style = GUI.Style_HTML |
275 var offset = 0 |
276 var offset = 0 |
276 for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { |
277 for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { |
277 val kind = chunk.kind |
278 val kind = chunk.kind |
278 val name = chunk.name |
279 val name = chunk.name |
279 val source = chunk.source |
280 val source = chunk.source |
280 if (kind != "") { |
281 if (kind != "") { |
281 val label = kind + if_proper(name, " " + name) |
282 val label = kind + if_proper(name, " " + name) |
282 val label_html = |
283 val label_html = style.enclose(GUI.Name(name, kind = kind, style = style).toString) |
283 "<html><b>" + HTML.output(kind) + "</b>" + |
|
284 if_proper(name, " " + HTML.output(name)) + "</html>" |
|
285 val range = Text.Range(offset, offset + source.length) |
284 val range = Text.Range(offset, offset + source.length) |
286 val asset = new Asset(label, label_html, range, source) |
285 val asset = new Asset(label, label_html, range, source) |
287 data.root.add(Tree_View.Node(asset)) |
286 data.root.add(Tree_View.Node(asset)) |
288 } |
287 } |
289 offset += source.length |
288 offset += source.length |