--- a/src/Pure/Tools/bibtex.scala Sat Jan 07 21:32:00 2017 +0100
+++ b/src/Pure/Tools/bibtex.scala Sun Jan 08 10:56:33 2017 +0100
@@ -14,6 +14,27 @@
object Bibtex
{
+ /** document model **/
+
+ 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)] =
+ {
+ val result = new mutable.ListBuffer[(String, Text.Offset)]
+ var offset = 0
+ for (chunk <- Bibtex.parse(text)) {
+ if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset))
+ offset += chunk.source.length
+ }
+ result.toList
+ }
+
+
+
/** content **/
private val months = List(
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Sat Jan 07 21:32:00 2017 +0100
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Sun Jan 08 10:56:33 2017 +0100
@@ -29,33 +29,6 @@
{
/** buffer model **/
- /* file type */
-
- def check(buffer: Buffer): Boolean =
- JEdit_Lib.buffer_name(buffer).endsWith(".bib")
-
- def check(name: Document.Node.Name): Boolean =
- name.node.endsWith(".bib")
-
-
- /* parse entries */
-
- def parse_entries(text: String): List[(String, Text.Offset)] =
- {
- val chunks =
- try { Bibtex.parse(text) }
- catch { case ERROR(msg) => Output.warning(msg); Nil }
-
- val result = new mutable.ListBuffer[(String, Text.Offset)]
- var offset = 0
- for (chunk <- chunks) {
- if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset))
- offset += chunk.source.length
- }
- result.toList
- }
-
-
/* retrieve entries */
def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
@@ -111,7 +84,7 @@
case text_area: TextArea =>
text_area.getBuffer match {
case buffer: Buffer
- if (check(buffer) && buffer.isEditable) =>
+ if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
val menu = new JMenu("BibTeX entries")
for (entry <- Bibtex.entries) {
val item = new JMenuItem(entry.kind)
--- a/src/Tools/jEdit/src/document_model.scala Sat Jan 07 21:32:00 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sun Jan 08 10:56:33 2017 +0100
@@ -187,7 +187,9 @@
{
lazy val bytes: Bytes = Bytes(text)
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
- lazy val bibtex_entries: List[(String, Text.Offset)] = Bibtex_JEdit.parse_entries(text)
+ lazy val bibtex_entries: List[(String, Text.Offset)] =
+ try { Bibtex.parse_entries(text) }
+ catch { case ERROR(msg) => Output.warning(msg); Nil }
}
}
@@ -248,7 +250,7 @@
else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
def bibtex_entries: List[(String, Text.Offset)] =
- if (Bibtex_JEdit.check(node_name)) content.bibtex_entries else Nil
+ if (Bibtex.check_name(node_name)) content.bibtex_entries else Nil
/* edits */
@@ -348,12 +350,14 @@
def bibtex_entries: List[(String, Text.Offset)] =
GUI_Thread.require {
- if (Bibtex_JEdit.check(buffer)) {
+ if (Bibtex.check_name(node_name)) {
_bibtex_entries match {
case Some(entries) => entries
case None =>
val text = JEdit_Lib.buffer_text(buffer)
- val entries = Bibtex_JEdit.parse_entries(text)
+ val entries =
+ try { Bibtex.parse_entries(text) }
+ catch { case ERROR(msg) => Output.warning(msg); Nil }
_bibtex_entries = Some(entries)
entries
}