author | wenzelm |
Tue, 21 Oct 2014 17:49:51 +0200 | |
changeset 58749 | 83b0f633190e |
parent 58549 | d4d97b79f1fb |
child 60878 | 1f0d2bbcf38b |
permissions | -rw-r--r-- |
56585 | 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 |
||
58548 | 13 |
import java.awt.event.MouseEvent |
14 |
||
15 |
import javax.swing.JMenuItem |
|
56585 | 16 |
|
17 |
import org.gjt.sp.jedit.gui.DynamicContextMenuService |
|
58548 | 18 |
import org.gjt.sp.jedit.textarea.JEditTextArea |
56585 | 19 |
|
20 |
||
21 |
class Context_Menu extends DynamicContextMenuService |
|
22 |
{ |
|
23 |
def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] = |
|
24 |
{ |
|
56588
272d173cd398
avoid conflict of Isabelle/jEdit popups with jEdit context menu;
wenzelm
parents:
56586
diff
changeset
|
25 |
PIDE.dismissed_popups(text_area.getView) |
58524 | 26 |
|
27 |
val items1 = |
|
28 |
if (evt != null && evt.getSource == text_area.getPainter) { |
|
29 |
val offset = text_area.xyToOffset(evt.getX, evt.getY) |
|
58549 | 30 |
if (offset >= 0) Spell_Checker.context_menu(text_area, offset) |
58524 | 31 |
else Nil |
56585 | 32 |
} |
58524 | 33 |
else Nil |
34 |
||
58548 | 35 |
val items2 = Bibtex_JEdit.context_menu(text_area) |
58524 | 36 |
|
37 |
val items = items1 ::: items2 |
|
38 |
if (items.isEmpty) null else items.toArray |
|
56585 | 39 |
} |
40 |
} |
|
41 |