# HG changeset patch
# User wenzelm
# Date 1483872078 -3600
# Node ID 07f209e957bc4e42a5ef09316a1b88b6eb765983
# Parent  e837f6bf653c0bce3795ea988e40a3cdb37803c4
refer to bibtex entries via general Document_Model, instead of editor buffers;

diff -r e837f6bf653c -r 07f209e957bc src/Tools/jEdit/src/bibtex_jedit.scala
--- a/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Jan 08 10:56:33 2017 +0100
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Jan 08 11:41:18 2017 +0100
@@ -27,26 +27,13 @@
 
 object Bibtex_JEdit
 {
-  /** buffer model **/
-
-  /* retrieve entries */
-
-  def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
-    for {
-      buffer <- JEdit_Lib.jedit_buffers()
-      model <- Document_Model.get(buffer).iterator
-      (name, offset) <- model.bibtex_entries.iterator
-    } yield (name, buffer, offset)
-
-
-  /* completion */
+  /** completion **/
 
   def complete(name: String): List[String] =
-  {
-    val name1 = name.toLowerCase
-    (for ((entry, _, _) <- entries_iterator() if entry.toLowerCase.containsSlice(name1))
-      yield entry).toList
-  }
+    (for {
+      (entry, _, _) <- Document_Model.bibtex_entries_iterator()
+      if entry.toLowerCase.containsSlice(name.toLowerCase)
+    } yield entry).toList
 
   def completion(
     history: Completion.History,
diff -r e837f6bf653c -r 07f209e957bc src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 10:56:33 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 11:41:18 2017 +0100
@@ -77,6 +77,12 @@
   def is_stable(): Boolean =
     state.value.models_iterator.forall(_.is_stable)
 
+  def bibtex_entries_iterator(): Iterator[(String, Document_Model, Text.Offset)] =
+    for {
+      model <- state.value.models_iterator
+      (entry, offset) <- model.bibtex_entries
+    } yield (entry, model, offset)
+
 
   /* init and exit */
 
@@ -193,7 +199,7 @@
   }
 }
 
-trait Document_Model extends Document.Model
+sealed abstract class Document_Model extends Document.Model
 {
   /* content */
 
@@ -245,6 +251,10 @@
 
   /* content */
 
+  def node_position(offset: Text.Offset): Line.Node_Position =
+    Line.Node_Position(node_name.node,
+      Line.Position.zero.advance(content.text.substring(0, offset), Text.Length))
+
   def get_blob: Option[Document.Blob] =
     if (is_theory) None
     else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
diff -r e837f6bf653c -r 07f209e957bc src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 10:56:33 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 11:41:18 2017 +0100
@@ -230,12 +230,6 @@
       override def toString: String = "URL " + quote(name)
     }
 
-  def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
-    new Hyperlink {
-      def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
-      override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
-    }
-
   def hyperlink_file(focus: Boolean, name: String): Hyperlink =
     hyperlink_file(focus, Line.Node_Position(name))
 
@@ -245,6 +239,20 @@
       override def toString: String = "file " + quote(pos.name)
     }
 
+  def hyperlink_model(focus: Boolean, model: Document_Model, offset: Text.Offset): Hyperlink =
+    model match {
+      case file_model: File_Model =>
+        val pos =
+          try { file_model.node_position(offset) }
+          catch { case ERROR(_) => Line.Node_Position(file_model.node_name.node) }
+        hyperlink_file(focus, pos)
+      case buffer_model: Buffer_Model =>
+        new Hyperlink {
+          def follow(view: View): Unit = goto_buffer(focus, view, buffer_model.buffer, offset)
+          override def toString: String = "buffer " + quote(model.node_name.node)
+        }
+    }
+
   def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset)
     : Option[Hyperlink] =
   {
diff -r e837f6bf653c -r 07f209e957bc src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Jan 08 10:56:33 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Jan 08 11:41:18 2017 +0100
@@ -413,9 +413,9 @@
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
             val opt_link =
-              Bibtex_JEdit.entries_iterator.collectFirst(
-                { case (a, buffer, offset) if a == name =>
-                    PIDE.editor.hyperlink_buffer(true, buffer, offset) })
+              Document_Model.bibtex_entries_iterator.collectFirst(
+                { case (a, model, offset) if a == name =>
+                    PIDE.editor.hyperlink_model(true, model, offset) })
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
 
           case _ => None