src/Tools/jEdit/src/context_menu.scala
changeset 58525 f008ceb3b046
parent 58524 f805b366a497
child 58526 f05ccce3eca2
equal deleted inserted replaced
58524:f805b366a497 58525:f008ceb3b046
    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 =