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

author	wenzelm
	Sat, 24 Jun 2017 11:02:32 +0200
changeset 66185	aa002ed3f6d1
parent 66180	201d42f67bba
child 66186	9de577f2dc3b
permissions	-rw-r--r--