src/Tools/jEdit/src/context_menu.scala
changeset 58546 72e2b2a609c4
parent 58543 9c1389befa56
child 58548 d0ee64efd624
equal deleted inserted replaced
58545:30b75b7958d6 58546:72e2b2a609c4
    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 (Isabelle.is_bibtex(buffer) && buffer.isEditable) =>
    78           if (Bibtex_JEdit.check(buffer) && 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.kind)
    81               val item = new JMenuItem(entry.kind)
    82               item.addActionListener(new ActionListener {
    82               item.addActionListener(new ActionListener {
    83                 def actionPerformed(evt: ActionEvent): Unit =
    83                 def actionPerformed(evt: ActionEvent): Unit =