# HG changeset patch
# User wenzelm
# Date 1412526643 -7200
# Node ID d0ee64efd6241d1a9119b75afff5f8698c67ff39
# Parent  6080615b8b9651e7098b6df9456622ae8c112581
clarified modules;

diff -r 6080615b8b96 -r d0ee64efd624 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 */
diff -r 6080615b8b96 -r d0ee64efd624 src/Tools/jEdit/src/context_menu.scala
--- a/src/Tools/jEdit/src/context_menu.scala	Sun Oct 05 18:21:39 2014 +0200
+++ b/src/Tools/jEdit/src/context_menu.scala	Sun Oct 05 18:30:43 2014 +0200
@@ -10,13 +10,14 @@
 import isabelle._
 
 
-import java.awt.event.{ActionListener, ActionEvent, MouseEvent}
-import javax.swing.{JMenu, JMenuItem}
+import java.awt.event.MouseEvent
+
+import javax.swing.JMenuItem
 
 import org.gjt.sp.jedit.menu.EnhancedMenuItem
 import org.gjt.sp.jedit.gui.DynamicContextMenuService
 import org.gjt.sp.jedit.{jEdit, Buffer}
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
+import org.gjt.sp.jedit.textarea.JEditTextArea
 
 
 class Context_Menu extends DynamicContextMenuService
@@ -67,32 +68,6 @@
   }
 
 
-  /* 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 (Bibtex_JEdit.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
-    }
-  }
-
-
   /* menu service */
 
   def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
@@ -107,7 +82,7 @@
       }
       else Nil
 
-    val items2 = bibtex_menu(text_area)
+    val items2 = Bibtex_JEdit.context_menu(text_area)
 
     val items = items1 ::: items2
     if (items.isEmpty) null else items.toArray