isabelle: src/Tools/jEdit/src/context_menu.scala@87ebf5a50283 (annotated)

56585 a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	1	/* Title: Tools/jEdit/src/context_menu.scala
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	2	Author: Makarius
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	3
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	4	Common context menu for Isabelle/jEdit.
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	5	*/
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	6
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	7	package isabelle.jedit
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	8
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	9
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	10	import isabelle._
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	11
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	12
58548 d0ee64efd624 clarified modules; wenzelm parents: 58546 diff changeset	13	import java.awt.event.MouseEvent
d0ee64efd624 clarified modules; wenzelm parents: 58546 diff changeset	14
d0ee64efd624 clarified modules; wenzelm parents: 58546 diff changeset	15	import javax.swing.JMenuItem
56585 a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	16
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	17	import org.gjt.sp.jedit.gui.DynamicContextMenuService
58548 d0ee64efd624 clarified modules; wenzelm parents: 58546 diff changeset	18	import org.gjt.sp.jedit.textarea.JEditTextArea
56585 a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	19
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	20
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 66120 diff changeset	21	class Context_Menu extends DynamicContextMenuService {
56585 a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	22	def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
62229 027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	23	if (evt == null) null
027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	24	else {
65240 fe5a96240749 clarified modules; wenzelm parents: 65139 diff changeset	25	Isabelle.dismissed_popups(text_area.getView)
58524 f805b366a497 context menu for bibtex entries; wenzelm parents: 56595 diff changeset	26
62229 027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	27	val items1 =
027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	28	if (evt != null && evt.getSource == text_area.getPainter) {
027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	29	val offset = text_area.xyToOffset(evt.getX, evt.getY)
027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	30	if (offset >= 0)
65139 0a2c0712e432 clarified modules: spell-checker in Pure; wenzelm parents: 62229 diff changeset	31	JEdit_Spell_Checker.context_menu(text_area, offset) :::
62229 027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	32	Debugger_Dockable.context_menu(text_area, offset)
027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	33	else Nil
027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	34	}
58524 f805b366a497 context menu for bibtex entries; wenzelm parents: 56595 diff changeset	35	else Nil
62229 027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	36
66120 e03ff7e831cc clarified modules; wenzelm parents: 65240 diff changeset	37	val items2 = JEdit_Bibtex.context_menu(text_area)
58524 f805b366a497 context menu for bibtex entries; wenzelm parents: 56595 diff changeset	38
62229 027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	39	val items = items1 ::: items2
027e6032977f more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; wenzelm parents: 60878 diff changeset	40	if (items.isEmpty) null else items.toArray
56585 a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	41	}
a0e844c6e1ed common context menu for Isabelle/jEdit; wenzelm parents: diff changeset	42	}

author	wenzelm
	Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393	87ebf5a50283
parent 66120	e03ff7e831cc
permissions	-rw-r--r--