equal
deleted
inserted
replaced
27 /** context menu **/ |
27 /** context menu **/ |
28 |
28 |
29 def context_menu(text_area: JEditTextArea): List[JMenuItem] = { |
29 def context_menu(text_area: JEditTextArea): List[JMenuItem] = { |
30 text_area.getBuffer match { |
30 text_area.getBuffer match { |
31 case buffer: Buffer |
31 case buffer: Buffer |
32 if Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable => |
32 if File.is_bib(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable => |
33 val menu = new JMenu("BibTeX entries") |
33 val menu = new JMenu("BibTeX entries") |
34 for (entry <- Bibtex.known_entries) { |
34 for (entry <- Bibtex.known_entries) { |
35 val item = new JMenuItem(entry.kind) |
35 val item = new JMenuItem(entry.kind) |
36 item.addActionListener(new ActionListener { |
36 item.addActionListener(new ActionListener { |
37 def actionPerformed(evt: ActionEvent): Unit = |
37 def actionPerformed(evt: ActionEvent): Unit = |