equal
deleted
inserted
replaced
73 { |
73 { |
74 text_area0 match { |
74 text_area0 match { |
75 case text_area: TextArea => |
75 case text_area: TextArea => |
76 text_area.getBuffer match { |
76 text_area.getBuffer match { |
77 case buffer: Buffer |
77 case buffer: Buffer |
78 if (JEdit_Lib.buffer_name(buffer).endsWith(".bib")) => |
78 if (JEdit_Lib.buffer_name(buffer).endsWith(".bib") && buffer.isEditable) => |
79 val menu = new JMenu("BibTeX entries") |
79 val menu = new JMenu("BibTeX entries") |
80 for (entry <- Bibtex.entries) { |
80 for (entry <- Bibtex.entries) { |
81 val item = new JMenuItem(entry.name) |
81 val item = new JMenuItem(entry.name) |
82 item.addActionListener(new ActionListener { |
82 item.addActionListener(new ActionListener { |
83 def actionPerformed(evt: ActionEvent): Unit = |
83 def actionPerformed(evt: ActionEvent): Unit = |