# HG changeset patch
# User wenzelm
# Date 1483869393 -3600
# Node ID e837f6bf653c0bce3795ea988e40a3cdb37803c4
# Parent  4ef1eb75f1cd370a0db17e2ef2299109c6591086
clarified modules;

diff -r 4ef1eb75f1cd -r e837f6bf653c src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Sat Jan 07 21:32:00 2017 +0100
+++ b/src/Pure/Tools/bibtex.scala	Sun Jan 08 10:56:33 2017 +0100
@@ -14,6 +14,27 @@
 
 object Bibtex
 {
+  /** document model **/
+
+  def check_name(name: String): Boolean = name.endsWith(".bib")
+  def check_name(name: Document.Node.Name): Boolean = check_name(name.node)
+
+
+  /* parse entries */
+
+  def parse_entries(text: String): List[(String, Text.Offset)] =
+  {
+    val result = new mutable.ListBuffer[(String, Text.Offset)]
+    var offset = 0
+    for (chunk <- Bibtex.parse(text)) {
+      if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset))
+      offset += chunk.source.length
+    }
+    result.toList
+  }
+
+
+
   /** content **/
 
   private val months = List(
diff -r 4ef1eb75f1cd -r e837f6bf653c src/Tools/jEdit/src/bibtex_jedit.scala
--- a/src/Tools/jEdit/src/bibtex_jedit.scala	Sat Jan 07 21:32:00 2017 +0100
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Jan 08 10:56:33 2017 +0100
@@ -29,33 +29,6 @@
 {
   /** buffer model **/
 
-  /* file type */
-
-  def check(buffer: Buffer): Boolean =
-    JEdit_Lib.buffer_name(buffer).endsWith(".bib")
-
-  def check(name: Document.Node.Name): Boolean =
-    name.node.endsWith(".bib")
-
-
-  /* parse entries */
-
-  def parse_entries(text: String): List[(String, Text.Offset)] =
-  {
-    val chunks =
-      try { Bibtex.parse(text) }
-      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
-  }
-
-
   /* retrieve entries */
 
   def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
@@ -111,7 +84,7 @@
       case text_area: TextArea =>
         text_area.getBuffer match {
           case buffer: Buffer
-          if (check(buffer) && buffer.isEditable) =>
+          if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
             val menu = new JMenu("BibTeX entries")
             for (entry <- Bibtex.entries) {
               val item = new JMenuItem(entry.kind)
diff -r 4ef1eb75f1cd -r e837f6bf653c src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 21:32:00 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 10:56:33 2017 +0100
@@ -187,7 +187,9 @@
   {
     lazy val bytes: Bytes = Bytes(text)
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
-    lazy val bibtex_entries: List[(String, Text.Offset)] = Bibtex_JEdit.parse_entries(text)
+    lazy val bibtex_entries: List[(String, Text.Offset)] =
+      try { Bibtex.parse_entries(text) }
+      catch { case ERROR(msg) => Output.warning(msg); Nil }
   }
 }
 
@@ -248,7 +250,7 @@
     else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
 
   def bibtex_entries: List[(String, Text.Offset)] =
-    if (Bibtex_JEdit.check(node_name)) content.bibtex_entries else Nil
+    if (Bibtex.check_name(node_name)) content.bibtex_entries else Nil
 
 
   /* edits */
@@ -348,12 +350,14 @@
 
   def bibtex_entries: List[(String, Text.Offset)] =
     GUI_Thread.require {
-      if (Bibtex_JEdit.check(buffer)) {
+      if (Bibtex.check_name(node_name)) {
         _bibtex_entries match {
           case Some(entries) => entries
           case None =>
             val text = JEdit_Lib.buffer_text(buffer)
-            val entries = Bibtex_JEdit.parse_entries(text)
+            val entries =
+              try { Bibtex.parse_entries(text) }
+              catch { case ERROR(msg) => Output.warning(msg); Nil }
             _bibtex_entries = Some(entries)
             entries
         }