--- 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
}
--- 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
--- 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
--- 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