--- a/src/Tools/jEdit/src/bibtex_jedit.scala Sun Oct 05 18:14:26 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Sun Oct 05 18:21:39 2014 +0200
@@ -10,6 +10,8 @@
import isabelle._
+import scala.collection.mutable
+
import javax.swing.text.Segment
import javax.swing.tree.DefaultMutableTreeNode
@@ -26,6 +28,21 @@
def check(buffer: Buffer): Boolean =
JEdit_Lib.buffer_name(buffer).endsWith(".bib")
+ def parse_buffer_entries(buffer: Buffer): List[(String, Text.Offset)] =
+ {
+ val chunks =
+ try { Bibtex.parse(JEdit_Lib.buffer_text(buffer)) }
+ catch { case ERROR(msg) => Output.warning(msg); Nil }
+
+ val result = new mutable.ListBuffer[(String, Text.Offset)]
+ var offset = 0
+ for (chunk <- chunks) {
+ if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset))
+ offset += chunk.source.length
+ }
+ result.toList
+ }
+
def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
for {
buffer <- JEdit_Lib.jedit_buffers()
--- a/src/Tools/jEdit/src/document_model.scala Sun Oct 05 18:14:26 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Sun Oct 05 18:21:39 2014 +0200
@@ -167,19 +167,7 @@
_bibtex match {
case Some(entries) => entries
case None =>
- val chunks =
- try { Bibtex.parse(JEdit_Lib.buffer_text(buffer)) }
- catch { case ERROR(msg) => Output.warning(msg); Nil }
- val entries =
- {
- val result = new mutable.ListBuffer[(String, Text.Offset)]
- var offset = 0
- for (chunk <- chunks) {
- if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset))
- offset += chunk.source.length
- }
- result.toList
- }
+ val entries = Bibtex_JEdit.parse_buffer_entries(buffer)
_bibtex = Some(entries)
entries
}