context menu for bibtex entries;

--- a/NEWS	Thu Oct 02 11:54:30 2014 +0200
+++ b/NEWS	Fri Oct 03 11:03:37 2014 +0200
@@ -15,6 +15,11 @@
 semantics due to external visual order vs. internal reverse order.
 
 
+*** Prover IDE -- Isabelle/Scala/jEdit ***
+
+* Support for BibTeX files: context menu.
+
+
 *** Pure ***
 
 * Command "class_deps" takes optional sort arguments constraining

--- a/src/Pure/Tools/bibtex.scala	Thu Oct 02 11:54:30 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala	Fri Oct 03 11:03:37 2014 +0200
@@ -31,81 +31,74 @@
 
   val commands = List("preamble", "string")
 
-  sealed case class Entry_Type(
+  sealed case class Entry(
+    name: String,
     required: List[String],
     optional_crossref: List[String],
     optional: List[String])
+  {
+    def fields: List[String] = required ::: optional_crossref ::: optional
+    def template: String =
+      "@" + name + "{,\n" + fields.map(x => "  " + x + " = {},\n").mkString + "}\n"
+  }
 
-  val entries =
-    Map[String, Entry_Type](
-      "Article" ->
-        Entry_Type(
-          List("author", "title"),
-          List("journal", "year"),
-          List("volume", "number", "pages", "month", "note")),
-      "InProceedings" ->
-        Entry_Type(
-          List("author", "title"),
-          List("booktitle", "year"),
-          List("editor", "volume", "number", "series", "pages", "month", "address",
-            "organization", "publisher", "note")),
-      "InCollection" ->
-        Entry_Type(
-          List("author", "title", "booktitle"),
-          List("publisher", "year"),
-          List("editor", "volume", "number", "series", "type", "chapter", "pages",
-            "edition", "month", "address", "note")),
-      "InBook" ->
-        Entry_Type(
-         List("author", "editor", "title", "chapter"),
-         List("publisher", "year"),
-         List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
-      "Proceedings" ->
-        Entry_Type(
-          List("title", "year"),
-          List(),
-          List("booktitle", "editor", "volume", "number", "series", "address", "month",
-            "organization", "publisher", "note")),
-      "Book" ->
-        Entry_Type(
-          List("author", "editor", "title"),
-          List("publisher", "year"),
-          List("volume", "number", "series", "address", "edition", "month", "note")),
-      "Booklet" ->
-        Entry_Type(
-          List("title"),
-          List(),
-          List("author", "howpublished", "address", "month", "year", "note")),
-      "PhdThesis" ->
-        Entry_Type(
-          List("author", "title", "school", "year"),
-          List(),
-          List("type", "address", "month", "note")),
-      "MastersThesis" ->
-        Entry_Type(
-          List("author", "title", "school", "year"),
-          List(),
-          List("type", "address", "month", "note")),
-      "TechReport" ->
-        Entry_Type(
-          List("author", "title", "institution", "year"),
-          List(),
-          List("type", "number", "address", "month", "note")),
-      "Manual" ->
-        Entry_Type(
-          List("title"),
-          List(),
-          List("author", "organization", "address", "edition", "month", "year", "note")),
-      "Unpublished" ->
-        Entry_Type(
-          List("author", "title", "note"),
-          List(),
-          List("month", "year")),
-      "Misc" ->
-        Entry_Type(
-          List(),
-          List(),
-          List("author", "title", "howpublished", "month", "year", "note")))
+  val entries: List[Entry] =
+    List(
+      Entry("Article",
+        List("author", "title"),
+        List("journal", "year"),
+        List("volume", "number", "pages", "month", "note")),
+      Entry("InProceedings",
+        List("author", "title"),
+        List("booktitle", "year"),
+        List("editor", "volume", "number", "series", "pages", "month", "address",
+          "organization", "publisher", "note")),
+      Entry("InCollection",
+        List("author", "title", "booktitle"),
+        List("publisher", "year"),
+        List("editor", "volume", "number", "series", "type", "chapter", "pages",
+          "edition", "month", "address", "note")),
+      Entry("InBook",
+        List("author", "editor", "title", "chapter"),
+        List("publisher", "year"),
+        List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
+      Entry("Proceedings",
+        List("title", "year"),
+        List(),
+        List("booktitle", "editor", "volume", "number", "series", "address", "month",
+          "organization", "publisher", "note")),
+      Entry("Book",
+        List("author", "editor", "title"),
+        List("publisher", "year"),
+        List("volume", "number", "series", "address", "edition", "month", "note")),
+      Entry("Booklet",
+        List("title"),
+        List(),
+        List("author", "howpublished", "address", "month", "year", "note")),
+      Entry("PhdThesis",
+        List("author", "title", "school", "year"),
+        List(),
+        List("type", "address", "month", "note")),
+      Entry("MastersThesis",
+        List("author", "title", "school", "year"),
+        List(),
+        List("type", "address", "month", "note")),
+      Entry("TechReport",
+        List("author", "title", "institution", "year"),
+        List(),
+        List("type", "number", "address", "month", "note")),
+      Entry("Manual",
+        List("title"),
+        List(),
+        List("author", "organization", "address", "edition", "month", "year", "note")),
+      Entry("Unpublished",
+        List("author", "title", "note"),
+        List(),
+        List("month", "year")),
+      Entry("Misc",
+        List(),
+        List(),
+        List("author", "title", "howpublished", "month", "year", "note")))
 
 
 

--- a/src/Tools/jEdit/src/context_menu.scala	Thu Oct 02 11:54:30 2014 +0200
+++ b/src/Tools/jEdit/src/context_menu.scala	Fri Oct 03 11:03:37 2014 +0200
@@ -10,13 +10,13 @@
 import isabelle._
 
 
-import java.awt.event.MouseEvent
-import javax.swing.JMenuItem
+import java.awt.event.{ActionListener, ActionEvent, MouseEvent}
+import javax.swing.{JMenu, JMenuItem}
 
 import org.gjt.sp.jedit.menu.EnhancedMenuItem
 import org.gjt.sp.jedit.gui.DynamicContextMenuService
-import org.gjt.sp.jedit.jEdit
-import org.gjt.sp.jedit.textarea.JEditTextArea
+import org.gjt.sp.jedit.{jEdit, Buffer}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 
 
 class Context_Menu extends DynamicContextMenuService
@@ -67,20 +67,50 @@
   }
 
 
+  /* bibtex menu */
+
+  def bibtex_menu(text_area0: JEditTextArea): List[JMenuItem] =
+  {
+    text_area0 match {
+      case text_area: TextArea =>
+        text_area.getBuffer match {
+          case buffer: Buffer
+          if (JEdit_Lib.buffer_name(buffer).endsWith(".bib")) =>
+            val menu = new JMenu("BibTeX entries")
+            for (entry <- Bibtex.entries) {
+              val item = new JMenuItem(entry.name)
+              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
+    }
+  }
+
+
   /* menu service */
 
   def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
   {
     PIDE.dismissed_popups(text_area.getView)
-    if (evt != null && evt.getSource == text_area.getPainter) {
-      val offset = text_area.xyToOffset(evt.getX, evt.getY)
-      if (offset >= 0) {
-        val items = spell_checker_menu(text_area, offset)
-        if (items.isEmpty) null else items.toArray
+
+    val items1 =
+      if (evt != null && evt.getSource == text_area.getPainter) {
+        val offset = text_area.xyToOffset(evt.getX, evt.getY)
+        if (offset >= 0) spell_checker_menu(text_area, offset)
+        else Nil
       }
-      else null
-    }
-    else null
+      else Nil
+
+    val items2 = bibtex_menu(text_area)
+
+    val items = items1 ::: items2
+    if (items.isEmpty) null else items.toArray
   }
 }