class Context_Menu extends DynamicContextMenuService { def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] = if (evt == null) null else {
Isabelle.dismissed_popups(text_area.getView)
val items1 = if (evt != null && evt.getSource == text_area.getPainter) { val offset = text_area.xyToOffset(evt.getX, evt.getY) if (offset >= 0)
JEdit_Spell_Checker.context_menu(text_area, offset) :::
Debugger_Dockable.context_menu(text_area, offset) else Nil
} else Nil
val items2 = JEdit_Bibtex.context_menu(text_area)
val items = items1 ::: items2 if (items.isEmpty) nullelse items.toArray
}
}
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.15Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.