# HG changeset patch
# User wenzelm
# Date 1412526099 -7200
# Node ID 6080615b8b9651e7098b6df9456622ae8c112581
# Parent  72e2b2a609c4c1c75617d1e1bc64df8a1ed140ba
clarified modules;

diff -r 72e2b2a609c4 -r 6080615b8b96 src/Tools/jEdit/src/bibtex_jedit.scala
--- 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()
diff -r 72e2b2a609c4 -r 6080615b8b96 src/Tools/jEdit/src/document_model.scala
--- 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
         }