equal
deleted
inserted
replaced
25 PIDE.dismissed_popups(text_area.getView) |
25 PIDE.dismissed_popups(text_area.getView) |
26 |
26 |
27 val items1 = |
27 val items1 = |
28 if (evt != null && evt.getSource == text_area.getPainter) { |
28 if (evt != null && evt.getSource == text_area.getPainter) { |
29 val offset = text_area.xyToOffset(evt.getX, evt.getY) |
29 val offset = text_area.xyToOffset(evt.getX, evt.getY) |
30 if (offset >= 0) Spell_Checker.context_menu(text_area, offset) |
30 if (offset >= 0) |
|
31 Spell_Checker.context_menu(text_area, offset) ::: |
|
32 Debugger_Dockable.context_menu(text_area, offset) |
31 else Nil |
33 else Nil |
32 } |
34 } |
33 else Nil |
35 else Nil |
34 |
36 |
35 val items2 = Bibtex_JEdit.context_menu(text_area) |
37 val items2 = Bibtex_JEdit.context_menu(text_area) |
36 |
38 |
37 val items = items1 ::: items2 |
39 val items = items1 ::: items2 |
38 if (items.isEmpty) null else items.toArray |
40 if (items.isEmpty) null else items.toArray |
39 } |
41 } |
40 } |
42 } |
41 |
|