changeset 58546 | 72e2b2a609c4 |
parent 58543 | 9c1389befa56 |
child 58548 | d0ee64efd624 |
--- a/src/Tools/jEdit/src/context_menu.scala Sun Oct 05 17:58:36 2014 +0200 +++ b/src/Tools/jEdit/src/context_menu.scala Sun Oct 05 18:14:26 2014 +0200 @@ -75,7 +75,7 @@ case text_area: TextArea => text_area.getBuffer match { case buffer: Buffer - if (Isabelle.is_bibtex(buffer) && buffer.isEditable) => + if (Bibtex_JEdit.check(buffer) && buffer.isEditable) => val menu = new JMenu("BibTeX entries") for (entry <- Bibtex.entries) { val item = new JMenuItem(entry.kind)