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 (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 = |