# HG changeset patch
# User wenzelm
# Date 1412514326 -7200
# Node ID 9c1389befa56ffdb72fe1be80c6e0cb1c80ce380
# Parent  19e062fbfea00f0150c26addfeb656037df3ff68
maintain Document_Model.bibtex_entries;
clarified Chunk predicates;

diff -r 19e062fbfea0 -r 9c1389befa56 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Sun Oct 05 13:16:24 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala	Sun Oct 05 15:05:26 2014 +0200
@@ -176,10 +176,8 @@
 
     def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
     def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
-    def is_command: Boolean =
-      Bibtex.is_command(kind) && name != "" && content.isDefined && !is_malformed
-    def is_entry: Boolean =
-      Bibtex.is_entry(kind) && name != "" && content.isDefined && !is_malformed
+    def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
+    def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined
   }
 
 
diff -r 19e062fbfea0 -r 9c1389befa56 src/Tools/jEdit/src/context_menu.scala
--- a/src/Tools/jEdit/src/context_menu.scala	Sun Oct 05 13:16:24 2014 +0200
+++ b/src/Tools/jEdit/src/context_menu.scala	Sun Oct 05 15:05:26 2014 +0200
@@ -75,7 +75,7 @@
       case text_area: TextArea =>
         text_area.getBuffer match {
           case buffer: Buffer
-          if (JEdit_Lib.buffer_name(buffer).endsWith(".bib") && buffer.isEditable) =>
+          if (Isabelle.is_bibtex(buffer) && buffer.isEditable) =>
             val menu = new JMenu("BibTeX entries")
             for (entry <- Bibtex.entries) {
               val item = new JMenuItem(entry.kind)
diff -r 19e062fbfea0 -r 9c1389befa56 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Oct 05 13:16:24 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Oct 05 15:05:26 2014 +0200
@@ -155,6 +155,39 @@
     }
 
 
+  /* bibtex entries */
+
+  private var _bibtex: Option[List[(String, Text.Offset)]] = None  // owned by GUI thread
+
+  private def reset_bibtex(): Unit = GUI_Thread.require { _bibtex = None }
+
+  def bibtex_entries(): List[(String, Text.Offset)] =
+    GUI_Thread.require {
+      if (Isabelle.is_bibtex(buffer)) {
+        _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
+            }
+            _bibtex = Some(entries)
+            entries
+        }
+      }
+      else Nil
+    }
+
+
   /* edits */
 
   def node_edits(
@@ -211,6 +244,7 @@
     def edit(clear: Boolean, e: Text.Edit)
     {
       reset_blob()
+      reset_bibtex()
 
       if (clear) {
         pending_clear = true
diff -r 19e062fbfea0 -r 9c1389befa56 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Sun Oct 05 13:16:24 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Sun Oct 05 15:05:26 2014 +0200
@@ -64,6 +64,12 @@
     }
 
 
+  /* buffer types */
+
+  def is_bibtex(buffer: Buffer): Boolean =
+    JEdit_Lib.buffer_name(buffer).endsWith(".bib")
+
+
   /* token markers */
 
   private val markers: Map[String, TokenMarker] =