--- 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,
--- 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))
--- 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] =
{
--- 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