isabelle: src/Tools/jEdit/src/completion_popup.scala@1046a69fabaa (annotated)

53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	1	/* Title: Tools/jEdit/src/completion_popup.scala
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	2	Author: Makarius
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	3
53246 8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); wenzelm parents: 53244 diff changeset	4	Completion popup.
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	5	*/
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	6
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	7	package isabelle.jedit
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	8
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	9
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	10	import isabelle._
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	11
53297 64c31de7f21c border as for Pretty_Tooltip; wenzelm parents: 53296 diff changeset	12	import java.awt.{Color, Font, Point, BorderLayout, Dimension}
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 71383 diff changeset	13	import java.awt.event.{KeyEvent, KeyListener, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
56843 b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	14	import java.io.{File => JFile}
53246 8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); wenzelm parents: 53244 diff changeset	15	import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
53297 64c31de7f21c border as for Pretty_Tooltip; wenzelm parents: 53296 diff changeset	16	import javax.swing.border.LineBorder
53848 8d7029eb0c31 disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly; wenzelm parents: 53784 diff changeset	17	import javax.swing.text.DefaultCaret
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	18
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	19	import scala.swing.{ListView, ScrollPane}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	20	import scala.swing.event.MouseClicked
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	21	import org.gjt.sp.jedit.View
56325 ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	22	import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection}
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	23	import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
56843 b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	24	import org.gjt.sp.util.StandardUtilities
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	25
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	26
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	27	object Completion_Popup {
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	28	/ items with HTML rendering /
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	29
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	30	private class Item(val item: Completion.Item) {
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	31	private val html =
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	32	item.description match {
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	33	case a :: bs =>
63528 0f39f59317c1 completion templates for commands involving "begin ... end" blocks; wenzelm parents: 62113 diff changeset	34	"<html><b>" + HTML.output(Symbol.print_newlines(a)) + "</b>" +
0f39f59317c1 completion templates for commands involving "begin ... end" blocks; wenzelm parents: 62113 diff changeset	35	HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "</html>"
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	36	case Nil => ""
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	37	}
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	38	override def toString: String = html
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	39	}
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	40
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	41
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	42
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	43	/ jEdit text area /
53235 1b6a44859549 register single instance within root, in order to get rid of old popup as user continues typing; wenzelm parents: 53234 diff changeset	44
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	45	object Text_Area {
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	46	private val key = new Object
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	47
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	48	def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] = {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	49	GUI_Thread.require {}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	50	text_area.getClientProperty(key) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	51	case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	52	case _ => None
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	53	}
55712 e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	54	}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	55
55712 e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	56	def active_range(text_area: TextArea): Option[Text.Range] =
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	57	apply(text_area) match {
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	58	case Some(text_area_completion) => text_area_completion.active_range
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	59	case None => None
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	60	}
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	61
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	62	def action(text_area: TextArea, word_only: Boolean): Boolean =
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	63	apply(text_area) match {
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	64	case Some(text_area_completion) =>
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	65	if (text_area_completion.active_range.isDefined)
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	66	text_area_completion.action(word_only = word_only)
56177 bfa9dfb722de proper flags for main action (amending 638b29331549); wenzelm parents: 56175 diff changeset	67	else
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	68	text_area_completion.action(immediate = true, explicit = true, word_only = word_only)
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	69	true
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	70	case None => false
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	71	}
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	72
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	73	def exit(text_area: JEditTextArea): Unit = {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	74	GUI_Thread.require {}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	75	apply(text_area) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	76	case None =>
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	77	case Some(text_area_completion) =>
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	78	text_area_completion.deactivate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	79	text_area.putClientProperty(key, null)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	80	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	81	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	82
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	83	def init(text_area: JEditTextArea): Completion_Popup.Text_Area = {
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	84	exit(text_area)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	85	val text_area_completion = new Text_Area(text_area)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	86	text_area.putClientProperty(key, text_area_completion)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	87	text_area_completion.activate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	88	text_area_completion
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	89	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	90
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	91	def dismissed(text_area: TextArea): Boolean = {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	92	GUI_Thread.require {}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	93	apply(text_area) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	94	case Some(text_area_completion) => text_area_completion.dismissed()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	95	case None => false
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	96	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	97	}
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	98	}
0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	99
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	100	class Text_Area private(text_area: JEditTextArea) {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	101	// owned by GUI thread
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	102	private var completion_popup: Option[Completion_Popup] = None
0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	103
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	104	def active_range: Option[Text.Range] =
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	105	completion_popup match {
56605 46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	106	case Some(completion) => completion.active_range
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	107	case None => None
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	108	}
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	109
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	110
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	111	/* rendering */
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	112
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	113	def rendering(rendering: JEdit_Rendering, line_range: Text.Range): Option[Text.Info[Color]] = {
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	114	active_range match {
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	115	case Some(range) => range.try_restrict(line_range)
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	116	case None =>
66117 e6f808d1307c tuned signature; wenzelm parents: 66114 diff changeset	117	val caret = text_area.getCaretPosition
e6f808d1307c tuned signature; wenzelm parents: 66114 diff changeset	118	if (line_range.contains(caret)) {
e6f808d1307c tuned signature; wenzelm parents: 66114 diff changeset	119	rendering.before_caret_range(caret).try_restrict(line_range) match {
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	120	case Some(range) if !range.is_singularity =>
61601 15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	121	val range0 =
66157 cb57fcdbaf70 tuned signature; wenzelm parents: 66152 diff changeset	122	Completion.Result.merge(Completion.History.empty,
61734 31633e503c17 more thorough completion rendering, e.g. "Un"; wenzelm parents: 61601 diff changeset	123	syntax_completion(Completion.History.empty, true, Some(rendering)),
77029 1046a69fabaa dismantle special treatment of citations in Isabelle/Scala; wenzelm parents: 76794 diff changeset	124	rendering.path_completion(caret))
61601 15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	125	.map(_.range)
15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	126	rendering.semantic_completion(range0, range) match {
15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	127	case None => range0
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	128	case Some(Text.Info(_, Completion.No_Completion)) => None
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	129	case Some(Text.Info(range1, _: Completion.Names)) => Some(range1)
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	130	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	131	case _ => None
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	132	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	133	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	134	else None
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	135	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	136	}.map(range => Text.Info(range, rendering.completion_color))
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	137
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	138
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	139	/* syntax completion */
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	140
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	141	def syntax_completion(
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	142	history: Completion.History,
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	143	explicit: Boolean,
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	144	opt_rendering: Option[JEdit_Rendering]
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	145	): Option[Completion.Result] = {
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	146	val buffer = text_area.getBuffer
66055 07175635f78c tuned; wenzelm parents: 66054 diff changeset	147	val unicode = Isabelle_Encoding.is_active(buffer)
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	148
59074 7836d927ffca tuned signature; wenzelm parents: 58767 diff changeset	149	Isabelle.buffer_syntax(buffer) match {
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	150	case Some(syntax) =>
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	151	val context =
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	152	(for {
83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	153	rendering <- opt_rendering
56842 b6e266574b26 yet another completion option, to imitate old less ambitious behavior; wenzelm parents: 56841 diff changeset	154	if PIDE.options.bool("jedit_completion_context")
66117 e6f808d1307c tuned signature; wenzelm parents: 66114 diff changeset	155	caret_range = rendering.before_caret_range(text_area.getCaretPosition)
66054 fb0eea226a4d more uniform syntax_completion + semantic_completion; wenzelm parents: 65999 diff changeset	156	context <- rendering.language_context(caret_range)
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	157	} yield context) getOrElse syntax.language_context
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	158
56589 71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line; wenzelm parents: 56587 diff changeset	159	val caret = text_area.getCaretPosition
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line; wenzelm parents: 56587 diff changeset	160	val line_range = JEdit_Lib.line_range(buffer, text_area.getCaretLine)
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line; wenzelm parents: 56587 diff changeset	161	val line_start = line_range.start
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line; wenzelm parents: 56587 diff changeset	162	for {
67014 e6a695d6a6b2 tuned signature; wenzelm parents: 67005 diff changeset	163	line_text <- JEdit_Lib.get_text(buffer, line_range)
56589 71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line; wenzelm parents: 56587 diff changeset	164	result <-
67005 11fca474d87a tuned signature; wenzelm parents: 67004 diff changeset	165	syntax.complete(
66055 07175635f78c tuned; wenzelm parents: 66054 diff changeset	166	history, unicode, explicit, line_start, line_text, caret - line_start, context)
56589 71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line; wenzelm parents: 56587 diff changeset	167	} yield result
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	168
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	169	case None => None
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	170	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	171	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	172
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	173
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	174	/* completion action: text area */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	175
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	176	private def insert(item: Completion.Item): Unit = {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	177	GUI_Thread.require {}
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	178
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	179	val buffer = text_area.getBuffer
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	180	val range = item.range
56863 5fdb61a9a010 allow empty original, e.g. path ""; wenzelm parents: 56844 diff changeset	181	if (buffer.isEditable) {
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	182	JEdit_Lib.buffer_edit(buffer) {
67014 e6a695d6a6b2 tuned signature; wenzelm parents: 67005 diff changeset	183	JEdit_Lib.get_text(buffer, range) match {
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	184	case Some(text) if text == item.original =>
56325 ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	185	text_area.getSelectionAtOffset(text_area.getCaretPosition) match {
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	186
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	187	/rectangular selection as "tall caret"/
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	188	case selection : Selection.Rect
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	189	if selection.getStart(buffer, text_area.getCaretLine) == range.stop =>
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	190	text_area.moveCaretPosition(range.stop)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	191	(0 until Character.codePointCount(item.original, 0, item.original.length))
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	192	.foreach(_ => text_area.backspace())
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	193	text_area.setSelectedText(selection, item.replacement)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	194	text_area.moveCaretPosition(text_area.getCaretPosition + item.move)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	195
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	196	/other selections: rectangular, multiple range, .../
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	197	case selection
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	198	if selection != null &&
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	199	selection.getStart(buffer, text_area.getCaretLine) == range.start &&
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	200	selection.getEnd(buffer, text_area.getCaretLine) == range.stop =>
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	201	text_area.moveCaretPosition(range.stop + item.move)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	202	text_area.getSelection.foreach(text_area.setSelectedText(_, item.replacement))
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	203
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	204	/no selection/
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	205	case _ =>
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	206	buffer.remove(range.start, range.length)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	207	buffer.insert(range.start, item.replacement)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	208	text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
66180 201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	209	Isabelle.indent_input(text_area)
56325 ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	210	}
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	211	case _ =>
142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	212	}
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	213	}
4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	214	}
4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	215	}
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	216
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	217	def action(
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	218	immediate: Boolean = false,
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	219	explicit: Boolean = false,
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	220	delayed: Boolean = false,
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	221	word_only: Boolean = false
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	222	): Boolean = {
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	223	val view = text_area.getView
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	224	val layered = view.getLayeredPane
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	225	val buffer = text_area.getBuffer
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	226	val painter = text_area.getPainter
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	227
65239 509a9b0ad02e avoid global variables with implicit initialization; wenzelm parents: 65139 diff changeset	228	val history = PIDE.plugin.completion_history.value
66055 07175635f78c tuned; wenzelm parents: 66054 diff changeset	229	val unicode = Isabelle_Encoding.is_active(buffer)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	230
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	231	def open_popup(result: Completion.Result): Unit = {
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	232	val font =
55825 694833e3e4a0 tuned signature -- separate module Font_Info; wenzelm parents: 55813 diff changeset	233	painter.getFont.deriveFont(
694833e3e4a0 tuned signature -- separate module Font_Info; wenzelm parents: 55813 diff changeset	234	Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale")))
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	235
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	236	val range = result.range
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	237
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	238	val loc1 = text_area.offsetToXY(range.start)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	239	if (loc1 != null) {
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	240	val loc2 =
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	241	SwingUtilities.convertPoint(painter,
58767 30766b5fd0e1 proper line height and text base line, like regular TextAreaPainter.PaintText; wenzelm parents: 58592 diff changeset	242	loc1.x, loc1.y + painter.getLineHeight, layered)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	243
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	244	val items = result.items.map(new Item(_))
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	245	val completion =
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	246	new Completion_Popup(Some(range), layered, loc2, font, items) {
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	247	override def complete(item: Completion.Item): Unit = {
65239 509a9b0ad02e avoid global variables with implicit initialization; wenzelm parents: 65139 diff changeset	248	PIDE.plugin.completion_history.update(item)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	249	insert(item)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	250	}
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	251	override def propagate(evt: KeyEvent): Unit = {
56840 879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT); wenzelm parents: 56662 diff changeset	252	if (view.getKeyEventInterceptor == null)
879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT); wenzelm parents: 56662 diff changeset	253	JEdit_Lib.propagate_key(view, evt)
879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT); wenzelm parents: 56662 diff changeset	254	else if (view.getKeyEventInterceptor == inner_key_listener) {
56197 416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	255	try {
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	256	view.setKeyEventInterceptor(null)
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	257	JEdit_Lib.propagate_key(view, evt)
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	258	}
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	259	finally {
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	260	if (isDisplayable) view.setKeyEventInterceptor(inner_key_listener)
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	261	}
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	262	}
56171 15351577da10 clarified key event propagation, in accordance to outer_key_listener; wenzelm parents: 56170 diff changeset	263	if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	264	}
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	265	override def shutdown(focus: Boolean): Unit = {
56197 416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	266	if (view.getKeyEventInterceptor == inner_key_listener)
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	267	view.setKeyEventInterceptor(null)
73367 77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73340 diff changeset	268	if (focus) text_area.requestFocus()
56606 68b7a6db4a32 avoid ooddity: invoke intended function instead of java.awt.Container.invalidate(); wenzelm parents: 56605 diff changeset	269	JEdit_Lib.invalidate_range(text_area, range)
56197 416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	270	}
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	271	}
57127 a406e15c3cf7 make double-sure that old popup is dismissed, before replacing it; wenzelm parents: 57051 diff changeset	272	dismissed()
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	273	completion_popup = Some(completion)
56197 416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	274	view.setKeyEventInterceptor(completion.inner_key_listener)
56606 68b7a6db4a32 avoid ooddity: invoke intended function instead of java.awt.Container.invalidate(); wenzelm parents: 56605 diff changeset	275	JEdit_Lib.invalidate_range(text_area, range)
56841 bc6faeadbf82 reduced cluttering of popups; wenzelm parents: 56840 diff changeset	276	Pretty_Tooltip.dismissed_all()
56197 416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	277	completion.show_popup(false)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	278	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	279	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	280
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	281	if (buffer.isEditable) {
66117 e6f808d1307c tuned signature; wenzelm parents: 66114 diff changeset	282	val caret = text_area.getCaretPosition
76765 c654103e9c9d more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch; wenzelm parents: 75807 diff changeset	283	val opt_rendering = Document_View.get_rendering(text_area)
61601 15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	284	val result0 = syntax_completion(history, explicit, opt_rendering)
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	285	val (no_completion, semantic_completion) = {
61601 15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	286	opt_rendering match {
15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	287	case Some(rendering) =>
66055 07175635f78c tuned; wenzelm parents: 66054 diff changeset	288	rendering.semantic_completion_result(history, unicode, result0.map(_.range),
66117 e6f808d1307c tuned signature; wenzelm parents: 66114 diff changeset	289	rendering.before_caret_range(caret))
61601 15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	290	case None => (false, None)
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	291	}
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	292	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	293	if (no_completion) false
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	294	else {
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	295	val result = {
61601 15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	296	val result1 =
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	297	if (word_only) None
61601 15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	298	else Completion.Result.merge(history, semantic_completion, result0)
56564 94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	299	opt_rendering match {
61601 15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	300	case None => result1
56564 94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	301	case Some(rendering) =>
66157 cb57fcdbaf70 tuned signature; wenzelm parents: 66152 diff changeset	302	Completion.Result.merge(history,
66151 26eecd42cbc5 tuned signature; wenzelm parents: 66120 diff changeset	303	result1,
26eecd42cbc5 tuned signature; wenzelm parents: 66120 diff changeset	304	JEdit_Spell_Checker.completion(rendering, explicit, caret),
77029 1046a69fabaa dismantle special treatment of citations in Isabelle/Scala; wenzelm parents: 76794 diff changeset	305	rendering.path_completion(caret))
56564 94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	306	}
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	307	}
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	308	result match {
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	309	case Some(result) =>
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	310	result.items match {
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	311	case List(item) if result.unique && item.immediate && immediate =>
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	312	insert(item)
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	313	true
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	314	case _ :: _ if !delayed =>
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	315	open_popup(result)
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	316	false
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	317	case _ => false
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	318	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	319	case None => false
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	320	}
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	321	}
55752 43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	322	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	323	else false
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	324	}
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	325
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	326
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	327	/* input key events */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	328
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	329	def input(evt: KeyEvent): Unit = {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	330	GUI_Thread.require {}
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	331
66180 201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	332	if (!evt.isConsumed) {
201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	333	val special = JEdit_Lib.special_key(evt)
201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	334
201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	335	if (PIDE.options.bool("jedit_completion")) {
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	336	dismissed()
66185 aa002ed3f6d1 clarified indentation; wenzelm parents: 66180 diff changeset	337	if (evt.getKeyChar != '\b') {
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	338	val immediate = PIDE.options.bool("jedit_completion_immediate")
53397 b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords; wenzelm parents: 53337 diff changeset	339	if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords; wenzelm parents: 53337 diff changeset	340	input_delay.revoke()
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	341	action(immediate = immediate)
53397 b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords; wenzelm parents: 53337 diff changeset	342	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	343	else {
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	344	if (!special && action(immediate = immediate, delayed = true))
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	345	input_delay.revoke()
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	346	else
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	347	input_delay.invoke()
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	348	}
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	349	}
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	350	}
66180 201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	351
66186 9de577f2dc3b clarified indentation; wenzelm parents: 66185 diff changeset	352	val selection = text_area.getSelection()
71383 8313dca6dee9 misc tuning, following hint by IntelliJ; wenzelm parents: 67014 diff changeset	353	if (!special && (selection == null \|\| selection.isEmpty))
66186 9de577f2dc3b clarified indentation; wenzelm parents: 66185 diff changeset	354	Isabelle.indent_input(text_area)
53228 f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	355	}
f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	356	}
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	357
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	358	private val input_delay =
71704 b9a5eb0f3b43 clarified modules; wenzelm parents: 71601 diff changeset	359	Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) {
53322 a4cd032172e0 allow short words for explicit completion; wenzelm parents: 53297 diff changeset	360	action()
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	361	}
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	362
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	363
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	364	/* dismiss popup */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	365
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	366	def dismissed(): Boolean = {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	367	GUI_Thread.require {}
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	368
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	369	completion_popup match {
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	370	case Some(completion) =>
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	371	completion.hide_popup()
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	372	completion_popup = None
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	373	true
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	374	case None =>
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	375	false
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	376	}
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	377	}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	378
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	379
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	380	/* activation */
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	381
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	382	private val outer_key_listener =
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 71383 diff changeset	383	JEdit_Lib.key_listener(key_typed = input)
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	384
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	385	private def activate(): Unit =
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	386	text_area.addKeyListener(outer_key_listener)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	387
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	388	private def deactivate(): Unit = {
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	389	dismissed()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	390	text_area.removeKeyListener(outer_key_listener)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	391	}
53228 f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	392	}
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	393
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	394
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	395
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	396	/ history text field /
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	397
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	398	class History_Text_Field(
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	399	name: String = null,
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	400	instant_popups: Boolean = false,
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	401	enter_adds_to_history: Boolean = true,
67004 af72fa58f71b clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps; wenzelm parents: 66186 diff changeset	402	syntax: Outer_Syntax = Outer_Syntax.empty) extends
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	403	HistoryTextField(name, instant_popups, enter_adds_to_history
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	404	) {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	405	text_field =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	406
53848 8d7029eb0c31 disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly; wenzelm parents: 53784 diff changeset	407	// see https://forums.oracle.com/thread/1361677
8d7029eb0c31 disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly; wenzelm parents: 53784 diff changeset	408	if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	409
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	410	// owned by GUI thread
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	411	private var completion_popup: Option[Completion_Popup] = None
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	412
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	413
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	414	/* dismiss */
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	415
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	416	private def dismissed(): Boolean = {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	417	completion_popup match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	418	case Some(completion) =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	419	completion.hide_popup()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	420	completion_popup = None
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	421	true
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	422	case None =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	423	false
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	424	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	425	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	426
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	427
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	428	/* insert */
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	429
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	430	private def insert(item: Completion.Item): Unit = {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	431	GUI_Thread.require {}
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	432
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	433	val range = item.range
56863 5fdb61a9a010 allow empty original, e.g. path ""; wenzelm parents: 56844 diff changeset	434	if (text_field.isEditable) {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	435	val content = text_field.getText
66114 c137a9f038a6 clarified signature; wenzelm parents: 66055 diff changeset	436	range.try_substring(content) match {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	437	case Some(text) if text == item.original =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	438	text_field.setText(
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	439	content.substring(0, range.start) +
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	440	item.replacement +
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	441	content.substring(range.stop))
19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	442	text_field.getCaret.setDot(range.start + item.replacement.length + item.move)
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	443	case _ =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	444	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	445	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	446	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	447
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	448
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	449	/* completion action: text field */
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	450
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	451	def action(): Unit = {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	452	GUI.layered_pane(text_field) match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	453	case Some(layered) if text_field.isEditable =>
65239 509a9b0ad02e avoid global variables with implicit initialization; wenzelm parents: 65139 diff changeset	454	val history = PIDE.plugin.completion_history.value
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	455
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	456	val caret = text_field.getCaret.getDot
55813 08a1c860bc12 allow completion within a word (or symbol), like semantic completion; wenzelm parents: 55767 diff changeset	457	val text = text_field.getText
55748 2e1398b484aa no word completion within word context; wenzelm parents: 55747 diff changeset	458
55749 75a48dc4383e tuned signature; wenzelm parents: 55748 diff changeset	459	val context = syntax.language_context
55748 2e1398b484aa no word completion within word context; wenzelm parents: 55747 diff changeset	460
67005 11fca474d87a tuned signature; wenzelm parents: 67004 diff changeset	461	syntax.complete(history, true, false, 0, text, caret, context) match {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	462	case Some(result) =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	463	val fm = text_field.getFontMetrics(text_field.getFont)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	464	val loc =
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	465	SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	466
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	467	val items = result.items.map(new Item(_))
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	468	val completion =
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	469	new Completion_Popup(None, layered, loc, text_field.getFont, items) {
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	470	override def complete(item: Completion.Item): Unit = {
65239 509a9b0ad02e avoid global variables with implicit initialization; wenzelm parents: 65139 diff changeset	471	PIDE.plugin.completion_history.update(item)
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	472	insert(item)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	473	}
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	474	override def propagate(evt: KeyEvent): Unit =
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	475	if (!evt.isConsumed) text_field.processKeyEvent(evt)
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	476	override def shutdown(focus: Boolean): Unit =
73367 77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73340 diff changeset	477	if (focus) text_field.requestFocus()
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	478	}
57127 a406e15c3cf7 make double-sure that old popup is dismissed, before replacing it; wenzelm parents: 57051 diff changeset	479	dismissed()
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	480	completion_popup = Some(completion)
56197 416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	481	completion.show_popup(true)
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	482
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	483	case None =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	484	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	485	case _ =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	486	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	487	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	488
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	489
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	490	/* process key event */
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	491
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	492	private def process(evt: KeyEvent): Unit = {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	493	if (PIDE.options.bool("jedit_completion")) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	494	dismissed()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	495	if (evt.getKeyChar != '\b') {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	496	val special = JEdit_Lib.special_key(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	497	if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	498	process_delay.revoke()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	499	action()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	500	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	501	else process_delay.invoke()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	502	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	503	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	504	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	505
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	506	private val process_delay =
71704 b9a5eb0f3b43 clarified modules; wenzelm parents: 71601 diff changeset	507	Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	508	action()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	509	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	510
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	511	override def processKeyEvent(evt0: KeyEvent): Unit = {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	512	val evt = KeyEventWorkaround.processKeyEvent(evt0)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	513	if (evt != null) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	514	evt.getID match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	515	case KeyEvent.KEY_PRESSED =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	516	val key_code = evt.getKeyCode
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	517	if (key_code == KeyEvent.VK_ESCAPE) {
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	518	if (dismissed()) evt.consume()
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	519	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	520	case KeyEvent.KEY_TYPED =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	521	super.processKeyEvent(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	522	process(evt)
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	523	evt.consume()
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	524	case _ =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	525	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	526	if (!evt.isConsumed) super.processKeyEvent(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	527	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	528	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	529	}
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	530	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	531
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	532
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	533	class Completion_Popup private(
56605 46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	534	opt_range: Option[Text.Range],
53246 8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); wenzelm parents: 53244 diff changeset	535	layered: JLayeredPane,
8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); wenzelm parents: 53244 diff changeset	536	location: Point,
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	537	font: Font,
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	538	items: List[Completion_Popup.Item]
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	539	) extends JPanel(new BorderLayout) {
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	540	completion =>
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	541
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	542	GUI_Thread.require {}
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	543
73120 c3589f2dff31 more informative errors: simplify diagnosis of spurious failures reported by users; wenzelm parents: 72974 diff changeset	544	require(items.nonEmpty, "no completion items")
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 71383 diff changeset	545	val multi: Boolean = items.length > 1
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	546
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	547
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	548	/* actions */
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	549
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	550	def complete(item: Completion.Item): Unit = {}
0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	551	def propagate(evt: KeyEvent): Unit = {}
0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	552	def shutdown(focus: Boolean): Unit = {}
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	553
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	554
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	555	/* list view */
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	556
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	557	private val list_view = new ListView(items)
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	558	list_view.font = font
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	559	list_view.selection.intervalMode = ListView.IntervalMode.Single
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	560	list_view.peer.setFocusTraversalKeysEnabled(false)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	561	list_view.peer.setVisibleRowCount(items.length min 8)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	562	list_view.peer.setSelectedIndex(0)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	563
53398 f8b150e8778b remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list); wenzelm parents: 53397 diff changeset	564	for (cond <-
f8b150e8778b remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list); wenzelm parents: 53397 diff changeset	565	List(JComponent.WHEN_FOCUSED,
f8b150e8778b remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list); wenzelm parents: 53397 diff changeset	566	JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT,
f8b150e8778b remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list); wenzelm parents: 53397 diff changeset	567	JComponent.WHEN_IN_FOCUSED_WINDOW)) list_view.peer.setInputMap(cond, null)
f8b150e8778b remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list); wenzelm parents: 53397 diff changeset	568
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	569	private def complete_selected(): Boolean = {
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	570	list_view.selection.items.toList match {
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	571	case item :: _ => complete(item.item); true
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	572	case _ => false
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	573	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	574	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	575
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	576	private def move_items(n: Int): Unit = {
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	577	val i = list_view.peer.getSelectedIndex
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	578	val j = ((i + n) min (items.length - 1)) max 0
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	579	if (i != j) {
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	580	list_view.peer.setSelectedIndex(j)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	581	list_view.peer.ensureIndexIsVisible(j)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	582	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	583	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	584
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	585	private def move_pages(n: Int): Unit = {
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	586	val page_size = list_view.peer.getVisibleRowCount - 1
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	587	move_items(page_size * n)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	588	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	589
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	590
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	591	/* event handling */
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	592
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 71383 diff changeset	593	val inner_key_listener: KeyListener =
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	594	JEdit_Lib.key_listener(
75394 42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	595	key_pressed = { (e: KeyEvent) =>
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	596	if (!e.isConsumed) {
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	597	e.getKeyCode match {
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	598	case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") =>
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	599	if (complete_selected()) e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	600	hide_popup()
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	601	case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") =>
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	602	if (complete_selected()) e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	603	hide_popup()
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	604	case KeyEvent.VK_ESCAPE =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	605	hide_popup()
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	606	e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	607	case KeyEvent.VK_UP \| KeyEvent.VK_KP_UP if multi =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	608	move_items(-1)
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	609	e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	610	case KeyEvent.VK_DOWN \| KeyEvent.VK_KP_DOWN if multi =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	611	move_items(1)
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	612	e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	613	case KeyEvent.VK_PAGE_UP if multi =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	614	move_pages(-1)
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	615	e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	616	case KeyEvent.VK_PAGE_DOWN if multi =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	617	move_pages(1)
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	618	e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	619	case _ =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	620	if (e.isActionKey \|\| e.isAltDown \|\| e.isMetaDown \|\| e.isControlDown)
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	621	hide_popup()
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	622	}
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	623	}
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	624	propagate(e)
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	625	},
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 71383 diff changeset	626	key_typed = propagate
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	627	)
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	628
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	629	list_view.peer.addKeyListener(inner_key_listener)
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	630
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	631	list_view.peer.addMouseListener(new MouseAdapter {
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	632	override def mouseClicked(e: MouseEvent): Unit = {
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	633	if (complete_selected()) e.consume()
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	634	hide_popup()
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	635	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	636	})
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	637
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	638	list_view.peer.addFocusListener(new FocusAdapter {
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	639	override def focusLost(e: FocusEvent): Unit = hide_popup()
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	640	})
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	641
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	642
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	643	/* main content */
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	644
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	645	override def getFocusTraversalKeysEnabled = false
53297 64c31de7f21c border as for Pretty_Tooltip; wenzelm parents: 53296 diff changeset	646	completion.setBorder(new LineBorder(Color.BLACK))
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	647	completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	648
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	649
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	650	/* popup */
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	651
56605 46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	652	def active_range: Option[Text.Range] =
46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	653	if (isDisplayable) opt_range else None
46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	654
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	655	private val popup = {
72974 3afd293347cc clarified modules; wenzelm parents: 71704 diff changeset	656	val screen = GUI.screen_location(layered, location)
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	657	val size = {
53230 6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	658	val geometry = JEdit_Lib.window_geometry(completion, completion)
64621 7116f2634e32 clarified module name; wenzelm parents: 63674 diff changeset	659	val bounds = JEdit_Rendering.popup_bounds
53247 bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations; wenzelm parents: 53246 diff changeset	660	val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations; wenzelm parents: 53246 diff changeset	661	val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations; wenzelm parents: 53246 diff changeset	662	new Dimension(w, h)
53230 6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	663	}
53247 bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations; wenzelm parents: 53246 diff changeset	664	new Popup(layered, completion, screen.relative(layered, size), size)
53246 8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); wenzelm parents: 53244 diff changeset	665	}
8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); wenzelm parents: 53244 diff changeset	666
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	667	private def show_popup(focus: Boolean): Unit = {
53246 8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); wenzelm parents: 53244 diff changeset	668	popup.show
73367 77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73340 diff changeset	669	if (focus) list_view.requestFocus()
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	670	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	671
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	672	private def hide_popup(): Unit = {
56197 416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	673	shutdown(list_view.peer.isFocusOwner)
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; wenzelm parents: 56177 diff changeset	674	popup.hide
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	675	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	676	}

author	wenzelm
	Fri, 20 Jan 2023 20:26:42 +0100
changeset 77029	1046a69fabaa
parent 76794	941d4f527091
child 80225	d9ff4296e3b7
permissions	-rw-r--r--