--- a/src/Pure/PIDE/document.scala Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Pure/PIDE/document.scala Wed Jun 21 14:06:16 2017 +0200
@@ -502,6 +502,7 @@
def node_required: Boolean
def get_blob: Option[Blob]
+ def bibtex_entries: List[Text.Info[String]]
def node_edits(
node_header: Node.Header,
--- a/src/Pure/Tools/bibtex.scala Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Pure/Tools/bibtex.scala Wed Jun 21 14:06:16 2017 +0200
@@ -19,7 +19,7 @@
def check_name(name: String): Boolean = name.endsWith(".bib")
def check_name(name: Document.Node.Name): Boolean = check_name(name.node)
- def document_entries(text: String): List[Text.Info[String]] =
+ def entries(text: String): List[Text.Info[String]] =
{
val result = new mutable.ListBuffer[Text.Info[String]]
var offset = 0
@@ -32,6 +32,15 @@
result.toList
}
+ def entries_iterator[A, B <: Document.Model](models: Map[A, B])
+ : Iterator[Text.Info[(String, B)]] =
+ {
+ for {
+ (_, model) <- models.iterator
+ info <- model.bibtex_entries.iterator
+ } yield info.map((_, model))
+ }
+
/** content **/
@@ -69,7 +78,7 @@
"@" + kind + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n"
}
- val entries: List[Entry] =
+ val known_entries: List[Entry] =
List(
Entry("Article",
List("author", "title"),
@@ -128,7 +137,7 @@
List("author", "title", "howpublished", "month", "year", "note")))
def get_entry(kind: String): Option[Entry] =
- entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
+ known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
def is_entry(kind: String): Boolean = get_entry(kind).isDefined
--- a/src/Tools/VSCode/src/document_model.scala Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala Wed Jun 21 14:06:16 2017 +0200
@@ -43,7 +43,7 @@
lazy val bytes: Bytes = Bytes(text)
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
lazy val bibtex_entries: List[Text.Info[String]] =
- try { Bibtex.document_entries(text) }
+ try { Bibtex.entries(text) }
catch { case ERROR(_) => Nil }
}
@@ -133,6 +133,12 @@
else Some((Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty)))
+ /* bibtex entries */
+
+ def bibtex_entries: List[Text.Info[String]] =
+ model.content.bibtex_entries
+
+
/* edits */
def change_text(text: String, range: Option[Line.Range] = None): Option[Document_Model] =
--- a/src/Tools/VSCode/src/vscode_rendering.scala Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Jun 21 14:06:16 2017 +0200
@@ -303,7 +303,7 @@
case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
val iterator =
for {
- Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator
+ Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator()
if entry == name
} yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
--- a/src/Tools/VSCode/src/vscode_resources.scala Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Jun 21 14:06:16 2017 +0200
@@ -129,10 +129,7 @@
}
def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
- for {
- (_, model) <- state.value.models.iterator
- info <- model.content.bibtex_entries.iterator
- } yield info.map((_, model))
+ Bibtex.entries_iterator(state.value.models)
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
{
--- a/src/Tools/jEdit/src/document_model.scala Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Jun 21 14:06:16 2017 +0200
@@ -78,10 +78,7 @@
def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
- for {
- (_, model) <- state.value.models.iterator
- info <- model.bibtex_entries.iterator
- } yield info.map((_, model))
+ Bibtex.entries_iterator(state.value.models)
/* overlays */
@@ -275,7 +272,7 @@
lazy val bytes: Bytes = Bytes(Symbol.encode(text))
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
lazy val bibtex_entries: List[Text.Info[String]] =
- try { Bibtex.document_entries(text) }
+ try { Bibtex.entries(text) }
catch { case ERROR(msg) => Output.warning(msg); Nil }
}
@@ -551,7 +548,7 @@
case None =>
val text = JEdit_Lib.buffer_text(buffer)
val entries =
- try { Bibtex.document_entries(text) }
+ try { Bibtex.entries(text) }
catch { case ERROR(msg) => Output.warning(msg); Nil }
_bibtex_entries = Some(entries)
entries
--- a/src/Tools/jEdit/src/jedit_bibtex.scala Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala Wed Jun 21 14:06:16 2017 +0200
@@ -50,7 +50,7 @@
case buffer: Buffer
if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
val menu = new JMenu("BibTeX entries")
- for (entry <- Bibtex.entries) {
+ for (entry <- Bibtex.known_entries) {
val item = new JMenuItem(entry.kind)
item.addActionListener(new ActionListener {
def actionPerformed(evt: ActionEvent): Unit =
--- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Wed Jun 21 14:06:16 2017 +0200
@@ -259,7 +259,7 @@
case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
val opt_link =
- Document_Model.bibtex_entries_iterator.collectFirst(
+ Document_Model.bibtex_entries_iterator().collectFirst(
{ 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))