src/Tools/jEdit/src/context_menu.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 62229 027e6032977f
child 65139 0a2c0712e432
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/context_menu.scala
     2     Author:     Makarius
     3 
     4 Common context menu for Isabelle/jEdit.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 
    13 import java.awt.event.MouseEvent
    14 
    15 import javax.swing.JMenuItem
    16 
    17 import org.gjt.sp.jedit.gui.DynamicContextMenuService
    18 import org.gjt.sp.jedit.textarea.JEditTextArea
    19 
    20 
    21 class Context_Menu extends DynamicContextMenuService
    22 {
    23   def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
    24     if (evt == null) null
    25     else {
    26       PIDE.dismissed_popups(text_area.getView)
    27 
    28       val items1 =
    29         if (evt != null && evt.getSource == text_area.getPainter) {
    30           val offset = text_area.xyToOffset(evt.getX, evt.getY)
    31           if (offset >= 0)
    32             Spell_Checker.context_menu(text_area, offset) :::
    33             Debugger_Dockable.context_menu(text_area, offset)
    34           else Nil
    35         }
    36         else Nil
    37 
    38       val items2 = Bibtex_JEdit.context_menu(text_area)
    39 
    40       val items = items1 ::: items2
    41       if (items.isEmpty) null else items.toArray
    42   }
    43 }