isabelle: src/Tools/jEdit/src/completion_popup.scala@b0394e7d43ea (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)),
66158 ad83d4971dfe clarified modules; wenzelm parents: 66157 diff changeset	124	rendering.path_completion(caret),
66152 18e1aba549f6 tuned signature; wenzelm parents: 66151 diff changeset	125	Document_Model.bibtex_completion(Completion.History.empty, rendering, caret))
61601 15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	126	.map(_.range)
15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	127	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	128	case None => range0
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	129	case Some(Text.Info(_, Completion.No_Completion)) => None
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	130	case Some(Text.Info(range1, _: Completion.Names)) => Some(range1)
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	131	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	132	case _ => None
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	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	135	else None
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	136	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	137	}.map(range => Text.Info(range, rendering.completion_color))
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
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	140	/* syntax completion */
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	141
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	142	def syntax_completion(
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	143	history: Completion.History,
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	144	explicit: Boolean,
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	145	opt_rendering: Option[JEdit_Rendering]
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	146	): Option[Completion.Result] = {
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	147	val buffer = text_area.getBuffer
66055 07175635f78c tuned; wenzelm parents: 66054 diff changeset	148	val unicode = Isabelle_Encoding.is_active(buffer)
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	149
59074 7836d927ffca tuned signature; wenzelm parents: 58767 diff changeset	150	Isabelle.buffer_syntax(buffer) match {
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	151	case Some(syntax) =>
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	152	val context =
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	153	(for {
83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	154	rendering <- opt_rendering
56842 b6e266574b26 yet another completion option, to imitate old less ambitious behavior; wenzelm parents: 56841 diff changeset	155	if PIDE.options.bool("jedit_completion_context")
66117 e6f808d1307c tuned signature; wenzelm parents: 66114 diff changeset	156	caret_range = rendering.before_caret_range(text_area.getCaretPosition)
66054 fb0eea226a4d more uniform syntax_completion + semantic_completion; wenzelm parents: 65999 diff changeset	157	context <- rendering.language_context(caret_range)
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	158	} yield context) getOrElse syntax.language_context
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	159
56589 71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line; wenzelm parents: 56587 diff changeset	160	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	161	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	162	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	163	for {
67014 e6a695d6a6b2 tuned signature; wenzelm parents: 67005 diff changeset	164	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	165	result <-
67005 11fca474d87a tuned signature; wenzelm parents: 67004 diff changeset	166	syntax.complete(
66055 07175635f78c tuned; wenzelm parents: 66054 diff changeset	167	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	168	} yield result
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	169
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	170	case None => None
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
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	174
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	175	/* completion action: text area */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	176
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	177	private def insert(item: Completion.Item): Unit = {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	178	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	179
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	180	val buffer = text_area.getBuffer
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	181	val range = item.range
56863 5fdb61a9a010 allow empty original, e.g. path ""; wenzelm parents: 56844 diff changeset	182	if (buffer.isEditable) {
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	183	JEdit_Lib.buffer_edit(buffer) {
67014 e6a695d6a6b2 tuned signature; wenzelm parents: 67005 diff changeset	184	JEdit_Lib.get_text(buffer, range) match {
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	185	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	186	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	187
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	188	/rectangular selection as "tall caret"/
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	189	case selection : Selection.Rect
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	190	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	191	text_area.moveCaretPosition(range.stop)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	192	(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	193	.foreach(_ => text_area.backspace())
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	194	text_area.setSelectedText(selection, item.replacement)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	195	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	196
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	197	/other selections: rectangular, multiple range, .../
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	198	case selection
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	199	if selection != null &&
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	200	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	201	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	202	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	203	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	204
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	205	/no selection/
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	206	case _ =>
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	207	buffer.remove(range.start, range.length)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	208	buffer.insert(range.start, item.replacement)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	209	text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
66180 201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	210	Isabelle.indent_input(text_area)
56325 ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	211	}
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	212	case _ =>
142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	213	}
53233 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	}
4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	216	}
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	217
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	218	def action(
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	219	immediate: Boolean = false,
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	220	explicit: Boolean = false,
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	221	delayed: Boolean = false,
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	222	word_only: Boolean = false
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	223	): Boolean = {
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	224	val view = text_area.getView
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	225	val layered = view.getLayeredPane
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	226	val buffer = text_area.getBuffer
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	227	val painter = text_area.getPainter
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	228
65239 509a9b0ad02e avoid global variables with implicit initialization; wenzelm parents: 65139 diff changeset	229	val history = PIDE.plugin.completion_history.value
66055 07175635f78c tuned; wenzelm parents: 66054 diff changeset	230	val unicode = Isabelle_Encoding.is_active(buffer)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	231
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	232	def open_popup(result: Completion.Result): Unit = {
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	233	val font =
55825 694833e3e4a0 tuned signature -- separate module Font_Info; wenzelm parents: 55813 diff changeset	234	painter.getFont.deriveFont(
694833e3e4a0 tuned signature -- separate module Font_Info; wenzelm parents: 55813 diff changeset	235	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	236
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	237	val range = result.range
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	238
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	239	val loc1 = text_area.offsetToXY(range.start)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	240	if (loc1 != null) {
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	241	val loc2 =
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	242	SwingUtilities.convertPoint(painter,
58767 30766b5fd0e1 proper line height and text base line, like regular TextAreaPainter.PaintText; wenzelm parents: 58592 diff changeset	243	loc1.x, loc1.y + painter.getLineHeight, layered)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	244
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	245	val items = result.items.map(new Item(_))
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	246	val completion =
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	247	new Completion_Popup(Some(range), layered, loc2, font, items) {
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	248	override def complete(item: Completion.Item): Unit = {
65239 509a9b0ad02e avoid global variables with implicit initialization; wenzelm parents: 65139 diff changeset	249	PIDE.plugin.completion_history.update(item)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	250	insert(item)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	251	}
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	252	override def propagate(evt: KeyEvent): Unit = {
56840 879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT); wenzelm parents: 56662 diff changeset	253	if (view.getKeyEventInterceptor == null)
879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT); wenzelm parents: 56662 diff changeset	254	JEdit_Lib.propagate_key(view, evt)
879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT); wenzelm parents: 56662 diff changeset	255	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	256	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	257	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	258	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	259	}
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	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	261	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	262	}
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	263	}
56171 15351577da10 clarified key event propagation, in accordance to outer_key_listener; wenzelm parents: 56170 diff changeset	264	if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	265	}
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	266	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	267	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	268	view.setKeyEventInterceptor(null)
73367 77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73340 diff changeset	269	if (focus) text_area.requestFocus()
56606 68b7a6db4a32 avoid ooddity: invoke intended function instead of java.awt.Container.invalidate(); wenzelm parents: 56605 diff changeset	270	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	271	}
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	272	}
57127 a406e15c3cf7 make double-sure that old popup is dismissed, before replacing it; wenzelm parents: 57051 diff changeset	273	dismissed()
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	274	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	275	view.setKeyEventInterceptor(completion.inner_key_listener)
56606 68b7a6db4a32 avoid ooddity: invoke intended function instead of java.awt.Container.invalidate(); wenzelm parents: 56605 diff changeset	276	JEdit_Lib.invalidate_range(text_area, range)
56841 bc6faeadbf82 reduced cluttering of popups; wenzelm parents: 56840 diff changeset	277	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	278	completion.show_popup(false)
55693 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	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	281
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	282	if (buffer.isEditable) {
66117 e6f808d1307c tuned signature; wenzelm parents: 66114 diff changeset	283	val caret = text_area.getCaretPosition
64882 c3b42ac0cf81 tuned signature; wenzelm parents: 64621 diff changeset	284	val opt_rendering = Document_View.get(text_area).map(_.get_rendering())
61601 15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	285	val result0 = syntax_completion(history, explicit, opt_rendering)
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	286	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	287	opt_rendering match {
15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	288	case Some(rendering) =>
66055 07175635f78c tuned; wenzelm parents: 66054 diff changeset	289	rendering.semantic_completion_result(history, unicode, result0.map(_.range),
66117 e6f808d1307c tuned signature; wenzelm parents: 66114 diff changeset	290	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	291	case None => (false, None)
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	292	}
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	293	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	294	if (no_completion) false
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	295	else {
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	296	val result = {
61601 15952a05133c syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML; wenzelm parents: 59319 diff changeset	297	val result1 =
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	298	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	299	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	300	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	301	case None => result1
56564 94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	302	case Some(rendering) =>
66157 cb57fcdbaf70 tuned signature; wenzelm parents: 66152 diff changeset	303	Completion.Result.merge(history,
66151 26eecd42cbc5 tuned signature; wenzelm parents: 66120 diff changeset	304	result1,
26eecd42cbc5 tuned signature; wenzelm parents: 66120 diff changeset	305	JEdit_Spell_Checker.completion(rendering, explicit, caret),
66158 ad83d4971dfe clarified modules; wenzelm parents: 66157 diff changeset	306	rendering.path_completion(caret),
66152 18e1aba549f6 tuned signature; wenzelm parents: 66151 diff changeset	307	Document_Model.bibtex_completion(history, rendering, caret))
56564 94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	308	}
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	309	}
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	310	result match {
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	311	case Some(result) =>
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	312	result.items match {
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	313	case List(item) if result.unique && item.immediate && immediate =>
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	314	insert(item)
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	315	true
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	316	case _ :: _ if !delayed =>
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	317	open_popup(result)
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	318	false
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	319	case _ => false
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	320	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	321	case None => false
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	322	}
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	323	}
55752 43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	324	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	325	else false
53292 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
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	328
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	329	/* input key events */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	330
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	331	def input(evt: KeyEvent): Unit = {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	332	GUI_Thread.require {}
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	333
66180 201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	334	if (!evt.isConsumed) {
201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	335	val special = JEdit_Lib.special_key(evt)
201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	336
201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	337	if (PIDE.options.bool("jedit_completion")) {
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	338	dismissed()
66185 aa002ed3f6d1 clarified indentation; wenzelm parents: 66180 diff changeset	339	if (evt.getKeyChar != '\b') {
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	340	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	341	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	342	input_delay.revoke()
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	343	action(immediate = immediate)
53397 b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords; wenzelm parents: 53337 diff changeset	344	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	345	else {
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	346	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	347	input_delay.revoke()
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	348	else
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	349	input_delay.invoke()
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	350	}
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	351	}
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	352	}
66180 201d42f67bba indentation of keywords after input; wenzelm parents: 66158 diff changeset	353
66186 9de577f2dc3b clarified indentation; wenzelm parents: 66185 diff changeset	354	val selection = text_area.getSelection()
71383 8313dca6dee9 misc tuning, following hint by IntelliJ; wenzelm parents: 67014 diff changeset	355	if (!special && (selection == null \|\| selection.isEmpty))
66186 9de577f2dc3b clarified indentation; wenzelm parents: 66185 diff changeset	356	Isabelle.indent_input(text_area)
53228 f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	357	}
f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	358	}
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	359
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	360	private val input_delay =
71704 b9a5eb0f3b43 clarified modules; wenzelm parents: 71601 diff changeset	361	Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) {
53322 a4cd032172e0 allow short words for explicit completion; wenzelm parents: 53297 diff changeset	362	action()
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	363	}
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	364
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	365
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	366	/* dismiss popup */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	367
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	368	def dismissed(): Boolean = {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	369	GUI_Thread.require {}
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	370
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	371	completion_popup match {
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	372	case Some(completion) =>
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	373	completion.hide_popup()
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	374	completion_popup = None
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	375	true
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	376	case None =>
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	377	false
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	378	}
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	379	}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	380
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	/* activation */
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	383
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	384	private val outer_key_listener =
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 71383 diff changeset	385	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	386
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	387	private def activate(): Unit =
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	388	text_area.addKeyListener(outer_key_listener)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	389
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	390	private def deactivate(): Unit = {
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	391	dismissed()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	392	text_area.removeKeyListener(outer_key_listener)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	393	}
53228 f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	394	}
53784 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
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	/ history text field /
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	399
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	400	class History_Text_Field(
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	401	name: String = null,
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	402	instant_popups: Boolean = false,
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	403	enter_adds_to_history: Boolean = true,
67004 af72fa58f71b clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps; wenzelm parents: 66186 diff changeset	404	syntax: Outer_Syntax = Outer_Syntax.empty) extends
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	405	HistoryTextField(name, instant_popups, enter_adds_to_history
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	406	) {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	407	text_field =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	408
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	409	// 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	410	if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	411
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	412	// owned by GUI thread
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	413	private var completion_popup: Option[Completion_Popup] = None
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	414
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	415
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	416	/* dismiss */
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	417
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	418	private def dismissed(): Boolean = {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	419	completion_popup match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	420	case Some(completion) =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	421	completion.hide_popup()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	422	completion_popup = None
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	423	true
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	424	case None =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	425	false
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
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	429
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	430	/* insert */
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	431
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	432	private def insert(item: Completion.Item): Unit = {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	433	GUI_Thread.require {}
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	434
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	435	val range = item.range
56863 5fdb61a9a010 allow empty original, e.g. path ""; wenzelm parents: 56844 diff changeset	436	if (text_field.isEditable) {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	437	val content = text_field.getText
66114 c137a9f038a6 clarified signature; wenzelm parents: 66055 diff changeset	438	range.try_substring(content) match {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	439	case Some(text) if text == item.original =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	440	text_field.setText(
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	441	content.substring(0, range.start) +
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	442	item.replacement +
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	443	content.substring(range.stop))
19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	444	text_field.getCaret.setDot(range.start + item.replacement.length + item.move)
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	445	case _ =>
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	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	449
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	450
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	451	/* completion action: text field */
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	452
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	453	def action(): Unit = {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	454	GUI.layered_pane(text_field) match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	455	case Some(layered) if text_field.isEditable =>
65239 509a9b0ad02e avoid global variables with implicit initialization; wenzelm parents: 65139 diff changeset	456	val history = PIDE.plugin.completion_history.value
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	457
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	458	val caret = text_field.getCaret.getDot
55813 08a1c860bc12 allow completion within a word (or symbol), like semantic completion; wenzelm parents: 55767 diff changeset	459	val text = text_field.getText
55748 2e1398b484aa no word completion within word context; wenzelm parents: 55747 diff changeset	460
55749 75a48dc4383e tuned signature; wenzelm parents: 55748 diff changeset	461	val context = syntax.language_context
55748 2e1398b484aa no word completion within word context; wenzelm parents: 55747 diff changeset	462
67005 11fca474d87a tuned signature; wenzelm parents: 67004 diff changeset	463	syntax.complete(history, true, false, 0, text, caret, context) match {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	464	case Some(result) =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	465	val fm = text_field.getFontMetrics(text_field.getFont)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	466	val loc =
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	467	SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	468
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	469	val items = result.items.map(new Item(_))
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	470	val completion =
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	471	new Completion_Popup(None, layered, loc, text_field.getFont, items) {
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	472	override def complete(item: Completion.Item): Unit = {
65239 509a9b0ad02e avoid global variables with implicit initialization; wenzelm parents: 65139 diff changeset	473	PIDE.plugin.completion_history.update(item)
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	474	insert(item)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	475	}
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	476	override def propagate(evt: KeyEvent): Unit =
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	477	if (!evt.isConsumed) text_field.processKeyEvent(evt)
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	478	override def shutdown(focus: Boolean): Unit =
73367 77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73340 diff changeset	479	if (focus) text_field.requestFocus()
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	480	}
57127 a406e15c3cf7 make double-sure that old popup is dismissed, before replacing it; wenzelm parents: 57051 diff changeset	481	dismissed()
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	482	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	483	completion.show_popup(true)
53784 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 None =>
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	case _ =>
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
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	491
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	492	/* process key event */
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	493
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	494	private def process(evt: KeyEvent): Unit = {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	495	if (PIDE.options.bool("jedit_completion")) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	496	dismissed()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	497	if (evt.getKeyChar != '\b') {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	498	val special = JEdit_Lib.special_key(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	499	if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	500	process_delay.revoke()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	501	action()
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	else process_delay.invoke()
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	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	507
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	508	private val process_delay =
71704 b9a5eb0f3b43 clarified modules; wenzelm parents: 71601 diff changeset	509	Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	510	action()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	511	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	512
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	513	override def processKeyEvent(evt0: KeyEvent): Unit = {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	514	val evt = KeyEventWorkaround.processKeyEvent(evt0)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	515	if (evt != null) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	516	evt.getID match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	517	case KeyEvent.KEY_PRESSED =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	518	val key_code = evt.getKeyCode
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	519	if (key_code == KeyEvent.VK_ESCAPE) {
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	520	if (dismissed()) evt.consume()
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	521	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	522	case KeyEvent.KEY_TYPED =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	523	super.processKeyEvent(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	524	process(evt)
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	525	evt.consume()
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	526	case _ =>
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	if (!evt.isConsumed) super.processKeyEvent(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	529	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	530	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	531	}
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	532	}
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
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	534
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	535	class Completion_Popup private(
56605 46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	536	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	537	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	538	location: Point,
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	539	font: Font,
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	540	items: List[Completion_Popup.Item]
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	541	) 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	542	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	543
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	544	GUI_Thread.require {}
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	545
73120 c3589f2dff31 more informative errors: simplify diagnosis of spurious failures reported by users; wenzelm parents: 72974 diff changeset	546	require(items.nonEmpty, "no completion items")
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 71383 diff changeset	547	val multi: Boolean = items.length > 1
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	548
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	549
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	550	/* actions */
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	551
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	552	def complete(item: Completion.Item): Unit = {}
0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	553	def propagate(evt: KeyEvent): Unit = {}
0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	554	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	555
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	/* 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	558
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	private val list_view = new ListView(items)
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	560	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	561	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	562	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	563	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	564	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	565
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	566	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	567	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	568	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	569	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	570
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	571	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	572	list_view.selection.items.toList match {
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	573	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	574	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	575	}
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	576	}
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
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	578	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	579	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	580	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	581	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	582	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	583	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	584	}
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	585	}
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
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	587	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	588	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	589	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	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
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
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	593	/* 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	594
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 71383 diff changeset	595	val inner_key_listener: KeyListener =
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	596	JEdit_Lib.key_listener(
75394 42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	597	key_pressed = { (e: KeyEvent) =>
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	598	if (!e.isConsumed) {
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	599	e.getKeyCode match {
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	600	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	601	if (complete_selected()) e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	602	hide_popup()
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	603	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	604	if (complete_selected()) e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	605	hide_popup()
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	606	case KeyEvent.VK_ESCAPE =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	607	hide_popup()
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	608	e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	609	case KeyEvent.VK_UP \| KeyEvent.VK_KP_UP if multi =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	610	move_items(-1)
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	611	e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	612	case KeyEvent.VK_DOWN \| KeyEvent.VK_KP_DOWN if multi =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	613	move_items(1)
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	614	e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	615	case KeyEvent.VK_PAGE_UP if multi =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	616	move_pages(-1)
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	617	e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	618	case KeyEvent.VK_PAGE_DOWN if multi =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	619	move_pages(1)
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	620	e.consume()
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	621	case _ =>
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	622	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	623	hide_popup()
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	624	}
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	625	}
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	626	propagate(e)
87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	627	},
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 71383 diff changeset	628	key_typed = propagate
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	629	)
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
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	631	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	632
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	633	list_view.peer.addMouseListener(new MouseAdapter {
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	634	override def mouseClicked(e: MouseEvent): Unit = {
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75394 diff changeset	635	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	636	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	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	})
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	639
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	list_view.peer.addFocusListener(new FocusAdapter {
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 73120 diff changeset	641	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	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
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	/* 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	646
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	override def getFocusTraversalKeysEnabled = false
53297 64c31de7f21c border as for Pretty_Tooltip; wenzelm parents: 53296 diff changeset	648	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	649	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	650
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
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	652	/* 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	653
56605 46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	654	def active_range: Option[Text.Range] =
46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	655	if (isDisplayable) opt_range else None
46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	656
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	657	private val popup = {
72974 3afd293347cc clarified modules; wenzelm parents: 71704 diff changeset	658	val screen = GUI.screen_location(layered, location)
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	659	val size = {
53230 6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	660	val geometry = JEdit_Lib.window_geometry(completion, completion)
64621 7116f2634e32 clarified module name; wenzelm parents: 63674 diff changeset	661	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	662	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	663	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	664	new Dimension(w, h)
53230 6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	665	}
53247 bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations; wenzelm parents: 53246 diff changeset	666	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	667	}
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
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	669	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	670	popup.show
73367 77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73340 diff changeset	671	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	672	}
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	673
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73367 diff changeset	674	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	675	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	676	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	677	}
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	678	}

author	wenzelm
	Fri, 12 Aug 2022 11:18:22 +0200
changeset 75807	b0394e7d43ea
parent 75394	42267c650205
child 76765	c654103e9c9d
permissions	-rw-r--r--