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;
wenzelm@56585
     1
/*  Title:      Tools/jEdit/src/context_menu.scala
wenzelm@56585
     2
    Author:     Makarius
wenzelm@56585
     3
wenzelm@56585
     4
Common context menu for Isabelle/jEdit.
wenzelm@56585
     5
*/
wenzelm@56585
     6
wenzelm@56585
     7
package isabelle.jedit
wenzelm@56585
     8
wenzelm@56585
     9
wenzelm@56585
    10
import isabelle._
wenzelm@56585
    11
wenzelm@56585
    12
wenzelm@58548
    13
import java.awt.event.MouseEvent
wenzelm@58548
    14
wenzelm@58548
    15
import javax.swing.JMenuItem
wenzelm@56585
    16
wenzelm@56585
    17
import org.gjt.sp.jedit.gui.DynamicContextMenuService
wenzelm@58548
    18
import org.gjt.sp.jedit.textarea.JEditTextArea
wenzelm@56585
    19
wenzelm@56585
    20
wenzelm@56585
    21
class Context_Menu extends DynamicContextMenuService
wenzelm@56585
    22
{
wenzelm@56585
    23
  def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
wenzelm@62229
    24
    if (evt == null) null
wenzelm@62229
    25
    else {
wenzelm@62229
    26
      PIDE.dismissed_popups(text_area.getView)
wenzelm@58524
    27
wenzelm@62229
    28
      val items1 =
wenzelm@62229
    29
        if (evt != null && evt.getSource == text_area.getPainter) {
wenzelm@62229
    30
          val offset = text_area.xyToOffset(evt.getX, evt.getY)
wenzelm@62229
    31
          if (offset >= 0)
wenzelm@62229
    32
            Spell_Checker.context_menu(text_area, offset) :::
wenzelm@62229
    33
            Debugger_Dockable.context_menu(text_area, offset)
wenzelm@62229
    34
          else Nil
wenzelm@62229
    35
        }
wenzelm@58524
    36
        else Nil
wenzelm@62229
    37
wenzelm@62229
    38
      val items2 = Bibtex_JEdit.context_menu(text_area)
wenzelm@58524
    39
wenzelm@62229
    40
      val items = items1 ::: items2
wenzelm@62229
    41
      if (items.isEmpty) null else items.toArray
wenzelm@56585
    42
  }
wenzelm@56585
    43
}