# HG changeset patch # User wenzelm # Date 1513873719 -3600 # Node ID 318f44a5c164bbf215727a9559358103c58ea8a7 # Parent 6a93aaa3ed3666567dcb77caba828c9a09686129 tuned signature; diff -r 6a93aaa3ed36 -r 318f44a5c164 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Thu Dec 21 16:29:03 2017 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Thu Dec 21 17:28:39 2017 +0100 @@ -427,8 +427,10 @@ if (is_theory) None else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty)) + def is_bibtex: Boolean = Bibtex.check_name(node_name) + def bibtex_entries: List[Text.Info[String]] = - if (Bibtex.check_name(node_name)) content.bibtex_entries else Nil + if (is_bibtex) content.bibtex_entries else Nil /* edits */