--- a/src/Tools/jEdit/src/jedit_bibtex.scala Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala Thu Dec 28 21:45:28 2017 +0100
@@ -35,7 +35,7 @@
case text_area: TextArea =>
text_area.getBuffer match {
case buffer: Buffer
- if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
+ if (Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
val menu = new JMenu("BibTeX entries")
for (entry <- Bibtex.known_entries) {
val item = new JMenuItem(entry.kind)