# HG changeset patch
# User wenzelm
# Date 1483875105 -3600
# Node ID 4792ee012e94655dd79cbbbfdf3df2a36ea99738
# Parent  9bc44bef99e65721fd6357fbdd1aa37195072a18
tuned signature;

diff -r 9bc44bef99e6 -r 4792ee012e94 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Sun Jan 08 12:00:37 2017 +0100
+++ b/src/Pure/Tools/bibtex.scala	Sun Jan 08 12:31:45 2017 +0100
@@ -19,16 +19,15 @@
   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)] =
+  def document_entries(text: String): List[Text.Info[String]] =
   {
-    val result = new mutable.ListBuffer[(String, Text.Offset)]
+    val result = new mutable.ListBuffer[Text.Info[String]]
     var offset = 0
     for (chunk <- Bibtex.parse(text)) {
-      if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset))
-      offset += chunk.source.length
+      val end_offset = offset + chunk.source.length
+      if (chunk.name != "" && !chunk.is_command)
+        result += Text.Info(Text.Range(offset, end_offset), chunk.name)
+      offset = end_offset
     }
     result.toList
   }
diff -r 9bc44bef99e6 -r 4792ee012e94 src/Tools/jEdit/src/bibtex_jedit.scala
--- a/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Jan 08 12:00:37 2017 +0100
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Jan 08 12:31:45 2017 +0100
@@ -31,7 +31,7 @@
 
   def complete(name: String): List[String] =
     (for {
-      (entry, _, _) <- Document_Model.bibtex_entries_iterator()
+      Text.Info(_, (entry, _)) <- Document_Model.bibtex_entries_iterator()
       if entry.toLowerCase.containsSlice(name.toLowerCase)
     } yield entry).toList
 
diff -r 9bc44bef99e6 -r 4792ee012e94 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 12:00:37 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 12:31:45 2017 +0100
@@ -77,11 +77,11 @@
   def is_stable(): Boolean =
     state.value.models_iterator.forall(_.is_stable)
 
-  def bibtex_entries_iterator(): Iterator[(String, Document_Model, Text.Offset)] =
+  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
     for {
       model <- state.value.models_iterator
-      (entry, offset) <- model.bibtex_entries
-    } yield (entry, model, offset)
+      Text.Info(range, entry) <- model.bibtex_entries
+    } yield Text.Info(range, (entry, model))
 
 
   /* init and exit */
@@ -193,8 +193,8 @@
   {
     lazy val bytes: Bytes = Bytes(text)
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
-    lazy val bibtex_entries: List[(String, Text.Offset)] =
-      try { Bibtex.parse_entries(text) }
+    lazy val bibtex_entries: List[Text.Info[String]] =
+      try { Bibtex.document_entries(text) }
       catch { case ERROR(msg) => Output.warning(msg); Nil }
   }
 }
@@ -203,7 +203,7 @@
 {
   /* content */
 
-  def bibtex_entries: List[(String, Text.Offset)]
+  def bibtex_entries: List[Text.Info[String]]
 
 
   /* perspective */
@@ -259,7 +259,7 @@
     if (is_theory) None
     else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
 
-  def bibtex_entries: List[(String, Text.Offset)] =
+  def bibtex_entries: List[Text.Info[String]] =
     if (Bibtex.check_name(node_name)) content.bibtex_entries else Nil
 
 
@@ -354,11 +354,11 @@
 
   /* bibtex entries */
 
-  private var _bibtex_entries: Option[List[(String, Text.Offset)]] = None  // owned by GUI thread
+  private var _bibtex_entries: Option[List[Text.Info[String]]] = None  // owned by GUI thread
 
   private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
 
-  def bibtex_entries: List[(String, Text.Offset)] =
+  def bibtex_entries: List[Text.Info[String]] =
     GUI_Thread.require {
       if (Bibtex.check_name(node_name)) {
         _bibtex_entries match {
@@ -366,7 +366,7 @@
           case None =>
             val text = JEdit_Lib.buffer_text(buffer)
             val entries =
-              try { Bibtex.parse_entries(text) }
+              try { Bibtex.document_entries(text) }
               catch { case ERROR(msg) => Output.warning(msg); Nil }
             _bibtex_entries = Some(entries)
             entries
diff -r 9bc44bef99e6 -r 4792ee012e94 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Jan 08 12:00:37 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Jan 08 12:31:45 2017 +0100
@@ -414,8 +414,8 @@
           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
             val opt_link =
               Document_Model.bibtex_entries_iterator.collectFirst(
-                { case (a, model, offset) if a == name =>
-                    PIDE.editor.hyperlink_model(true, model, offset) })
+                { case Text.Info(entry_range, (entry, model)) if entry == name =>
+                    PIDE.editor.hyperlink_model(true, model, entry_range.start) })
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
 
           case _ => None