equal
deleted
inserted
replaced
229 val data = Isabelle_Sidekick.root_data(buffer) |
229 val data = Isabelle_Sidekick.root_data(buffer) |
230 |
230 |
231 try { |
231 try { |
232 var offset = 0 |
232 var offset = 0 |
233 for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { |
233 for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { |
234 val n = chunk.size |
234 val n = chunk.source.size |
235 chunk match { |
235 chunk match { |
236 case item: Bibtex.Item if item.is_wellformed => |
236 case item: Bibtex.Item if item.is_wellformed => |
237 val label = if (item.name == "") item.kind else item.kind + " " + item.name |
237 val label = if (item.name == "") item.kind else item.kind + " " + item.name |
238 val asset = new Isabelle_Sidekick.Asset(label, offset, offset + n) |
238 val asset = new Isabelle_Sidekick.Asset(label, offset, offset + n) |
239 data.root.add(new DefaultMutableTreeNode(asset)) |
239 data.root.add(new DefaultMutableTreeNode(asset)) |