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