src/Tools/jEdit/src/bibtex_jedit.scala

--- a/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Oct 05 18:21:39 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Oct 05 18:30:43 2014 +0200
@@ -12,10 +12,14 @@
 
 import scala.collection.mutable
 
+import java.awt.event.{ActionListener, ActionEvent}
+
 import javax.swing.text.Segment
 import javax.swing.tree.DefaultMutableTreeNode
+import javax.swing.{JMenu, JMenuItem}
 
 import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
 
 import sidekick.{SideKickParser, SideKickParsedData}
@@ -52,6 +56,33 @@
 
 
 
+  /** context menu **/
+
+  def context_menu(text_area0: JEditTextArea): List[JMenuItem] =
+  {
+    text_area0 match {
+      case text_area: TextArea =>
+        text_area.getBuffer match {
+          case buffer: Buffer
+          if (check(buffer) && buffer.isEditable) =>
+            val menu = new JMenu("BibTeX entries")
+            for (entry <- Bibtex.entries) {
+              val item = new JMenuItem(entry.kind)
+              item.addActionListener(new ActionListener {
+                def actionPerformed(evt: ActionEvent): Unit =
+                  Isabelle.insert_line_padding(text_area, entry.template)
+              })
+              menu.add(item)
+            }
+            List(menu)
+          case _ => Nil
+        }
+      case _ => Nil
+    }
+  }
+
+
+
   /** token markup **/
 
   /* token style */