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

author	wenzelm
	Sun, 10 Jan 2021 13:04:29 +0100
changeset 73120	c3589f2dff31
parent 72974	3afd293347cc
child 73340	0ffcad1f6130
permissions	-rw-r--r--