isabelle: src/Tools/jEdit/src/completion_popup.scala@4815429974fe (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}
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	15	import java.util.regex.Pattern
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	16	import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
53297 64c31de7f21c border as for Pretty_Tooltip; wenzelm parents: 53296 diff changeset	17	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	18	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	19
f127e949389f Completion popup 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.{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	21	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	22
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	23	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	24	import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection}
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	25	import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
56843 b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	26	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	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
f127e949389f Completion popup 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	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	30	{
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	31	/ items with HTML rendering /
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	32
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	33	private class Item(val item: Completion.Item)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	34	{
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	35	private val html =
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	36	item.description match {
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	37	case a :: bs =>
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	38	"<html><b>" + HTML.encode(a) + "</b>" +
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	39	HTML.encode(bs.map(" " + _).mkString) + "</html>"
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	40	case Nil => ""
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	41	}
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	42	override def toString: String = html
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
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	46
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	47	/ 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	48
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	49	object Text_Area
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	50	{
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	51	private val key = new Object
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	52
55712 e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	53	def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	54	{
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	55	GUI_Thread.require {}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	56	text_area.getClientProperty(key) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	57	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	58	case _ => None
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	59	}
55712 e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	60	}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	61
55712 e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	62	def active_range(text_area: TextArea): Option[Text.Range] =
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	63	apply(text_area) match {
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	64	case Some(text_area_completion) => text_area_completion.active_range
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	65	case None => None
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	66	}
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	67
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	68	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	69	apply(text_area) match {
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	70	case Some(text_area_completion) =>
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	71	if (text_area_completion.active_range.isDefined)
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	72	text_area_completion.action(word_only = word_only)
56177 bfa9dfb722de proper flags for main action (amending 638b29331549); wenzelm parents: 56175 diff changeset	73	else
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	74	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	75	true
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	76	case None => false
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	77	}
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	78
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	79	def exit(text_area: JEditTextArea)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	80	{
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	81	GUI_Thread.require {}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	82	apply(text_area) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	83	case None =>
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	84	case Some(text_area_completion) =>
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	85	text_area_completion.deactivate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	86	text_area.putClientProperty(key, null)
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
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	90	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	91	{
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	92	exit(text_area)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	93	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	94	text_area.putClientProperty(key, text_area_completion)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	95	text_area_completion.activate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	96	text_area_completion
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	97	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	98
55712 e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	99	def dismissed(text_area: TextArea): Boolean =
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	100	{
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	101	GUI_Thread.require {}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	102	apply(text_area) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	103	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	104	case None => false
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	105	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	106	}
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	107	}
0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	108
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	109	class Text_Area private(text_area: JEditTextArea)
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	110	{
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	111	// owned by GUI thread
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	112	private var completion_popup: Option[Completion_Popup] = None
0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	113
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	114	def active_range: Option[Text.Range] =
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	115	completion_popup match {
56605 46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	116	case Some(completion) => completion.active_range
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	117	case None => None
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	118	}
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	119
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	120
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	121	/* rendering */
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	122
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	123	def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	124	{
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	125	active_range match {
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	126	case Some(range) => range.try_restrict(line_range)
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	127	case None =>
55767 96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	128	if (line_range.contains(text_area.getCaretPosition)) {
56593 0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	129	JEdit_Lib.before_caret_range(text_area, rendering).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 =>
56173 62f10624339a tuned signature; wenzelm parents: 56171 diff changeset	131	rendering.semantic_completion(range) match {
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	132	case Some(Text.Info(_, Completion.No_Completion)) => None
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	133	case Some(Text.Info(range1, _: Completion.Names)) => Some(range1)
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	134	case None =>
56877 4e9d2eab9cfa more visual feedback on path_completion, at the risk of file-system access in GUI painting; wenzelm parents: 56863 diff changeset	135	Completion.Result.merge(Completion.History.empty,
4e9d2eab9cfa more visual feedback on path_completion, at the risk of file-system access in GUI painting; wenzelm parents: 56863 diff changeset	136	syntax_completion(Completion.History.empty, false, Some(rendering)),
4e9d2eab9cfa more visual feedback on path_completion, at the risk of file-system access in GUI painting; wenzelm parents: 56863 diff changeset	137	path_completion(rendering)).map(_.range)
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	138	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	139	case _ => None
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	140	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	141	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	142	else 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	}.map(range => Text.Info(range, rendering.completion_color))
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	145
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	146
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	147	/* syntax completion */
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	def syntax_completion(
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	150	history: Completion.History,
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	151	explicit: Boolean,
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	152	opt_rendering: Option[Rendering]): Option[Completion.Result] =
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	153	{
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	154	val buffer = text_area.getBuffer
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	155	val decode = Isabelle_Encoding.is_active(buffer)
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	Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	158	case Some(syntax) =>
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	159	val context =
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	160	(for {
83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	161	rendering <- opt_rendering
56842 b6e266574b26 yet another completion option, to imitate old less ambitious behavior; wenzelm parents: 56841 diff changeset	162	if PIDE.options.bool("jedit_completion_context")
56593 0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	163	range = JEdit_Lib.before_caret_range(text_area, rendering)
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	164	context <- rendering.language_context(range)
83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	165	} yield context) getOrElse syntax.language_context
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	166
56589 71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line; wenzelm parents: 56587 diff changeset	167	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	168	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	169	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	170	for {
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line; wenzelm parents: 56587 diff changeset	171	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	172	result <-
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line; wenzelm parents: 56587 diff changeset	173	syntax.completion.complete(
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	174	history, decode, 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	175	} yield result
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	176
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	177	case None => None
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	178	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	179	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	180
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	181
56564 94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	182	/* spell-checker completion */
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	183
57051 5e30ffe79980 spell-checker completion is restricted to explicit mode, to avoid odd effects with immediate edits vs. delayed language context markup, and occasional delays due to dictionary lookup of many variants; wenzelm parents: 56877 diff changeset	184	def spell_checker_completion(
5e30ffe79980 spell-checker completion is restricted to explicit mode, to avoid odd effects with immediate edits vs. delayed language context markup, and occasional delays due to dictionary lookup of many variants; wenzelm parents: 56877 diff changeset	185	explicit: Boolean,
5e30ffe79980 spell-checker completion is restricted to explicit mode, to avoid odd effects with immediate edits vs. delayed language context markup, and occasional delays due to dictionary lookup of many variants; wenzelm parents: 56877 diff changeset	186	rendering: Rendering): Option[Completion.Result] =
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	187	{
83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	188	for {
83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	189	spell_checker <- PIDE.spell_checker.get
57051 5e30ffe79980 spell-checker completion is restricted to explicit mode, to avoid odd effects with immediate edits vs. delayed language context markup, and occasional delays due to dictionary lookup of many variants; wenzelm parents: 56877 diff changeset	190	if explicit
56593 0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	191	range = JEdit_Lib.before_caret_range(text_area, rendering)
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	192	word <- Spell_Checker.current_word(text_area, rendering, range)
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	193	words = spell_checker.complete(word.info)
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	194	if !words.isEmpty
83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	195	descr = "(from dictionary " + quote(spell_checker.toString) + ")"
56593 0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	196	items =
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	197	words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	198	} yield Completion.Result(word.range, word.info, false, items)
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	199	}
56564 94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	200
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	201
56843 b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	202	/* path completion */
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	203
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	204	def path_completion(rendering: Rendering): Option[Completion.Result] =
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	205	{
56844 52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	206	def complete(text: String): List[(String, List[String])] =
56843 b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	207	{
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	208	try {
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	209	val path = Path.explode(text)
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	210	val (dir, base_name) =
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	211	if (text == "" \|\| text.endsWith("/")) (path, "")
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	212	else (path.dir, path.base.implode)
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	213
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	214	val directory =
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	215	new JFile(PIDE.resources.append(rendering.snapshot.node_name.master_dir, dir))
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	216	val files = directory.listFiles
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	217	if (files == null) Nil
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	218	else {
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	219	val ignore =
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	220	Library.space_explode(':', PIDE.options.string("jedit_completion_path_ignore")).
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	221	map(s => Pattern.compile(StandardUtilities.globToRE(s)))
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	222	(for {
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	223	file <- files.iterator
56844 52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	224
56843 b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	225	name = file.getName
56844 52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	226	if name.startsWith(base_name)
56843 b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	227	if !ignore.exists(pat => pat.matcher(name).matches)
56844 52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	228
52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	229	text1 = (dir + Path.basic(name)).implode_short
52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	230	if text != text1
52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	231
52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	232	is_dir = new JFile(directory, name).isDirectory
52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	233	replacement = text1 + (if (is_dir) "/" else "")
52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	234	descr = List(text1, if (is_dir) "(directory)" else "(file)")
52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	235	} yield (replacement, descr)).take(PIDE.options.int("completion_limit")).toList
56843 b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	236	}
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	237	}
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	238	catch { case ERROR(_) => Nil }
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	239	}
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	240
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	241	for {
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	242	r1 <- rendering.language_path(JEdit_Lib.before_caret_range(text_area, rendering))
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	243	s1 <- JEdit_Lib.try_get_text(text_area.getBuffer, r1)
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	244	s2 <- Library.try_unquote(s1)
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	245	r2 = Text.Range(r1.start + 1, r1.stop - 1)
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	246	if Path.is_valid(s2)
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	247	paths = complete(s2)
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	248	if !paths.isEmpty
56844 52e5bf245b2a standardize to implode_short form; wenzelm parents: 56843 diff changeset	249	items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false))
56843 b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	250	} yield Completion.Result(r2, s2, false, items)
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	251	}
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	252
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	253
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	254	/* completion action: text area */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	255
53275 b34aac6511ab tuned signature; wenzelm parents: 53274 diff changeset	256	private def insert(item: Completion.Item)
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	257	{
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	258	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	259
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	260	val buffer = text_area.getBuffer
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	261	val range = item.range
56863 5fdb61a9a010 allow empty original, e.g. path ""; wenzelm parents: 56844 diff changeset	262	if (buffer.isEditable) {
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	263	JEdit_Lib.buffer_edit(buffer) {
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	264	JEdit_Lib.try_get_text(buffer, range) match {
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	265	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	266	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	267
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	268	/rectangular selection as "tall caret"/
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	269	case selection : Selection.Rect
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	270	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	271	text_area.moveCaretPosition(range.stop)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	272	(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	273	.foreach(_ => text_area.backspace())
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	274	text_area.setSelectedText(selection, item.replacement)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	275	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	276
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	277	/other selections: rectangular, multiple range, .../
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	278	case selection
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	279	if selection != null &&
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	280	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	281	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	282	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	283	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	284
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	285	/no selection/
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	286	case _ =>
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	287	buffer.remove(range.start, range.length)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	288	buffer.insert(range.start, item.replacement)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	289	text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing; wenzelm parents: 56197 diff changeset	290	}
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	291	case _ =>
142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	292	}
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	293	}
4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	294	}
4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	295	}
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	296
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	297	def action(
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	298	immediate: Boolean = false,
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	299	explicit: Boolean = false,
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	300	delayed: Boolean = false,
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	301	word_only: Boolean = false): Boolean =
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	302	{
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	303	val view = text_area.getView
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	304	val layered = view.getLayeredPane
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	305	val buffer = text_area.getBuffer
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	306	val painter = text_area.getPainter
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	307
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	308	val history = PIDE.completion_history.value
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	309	val decode = Isabelle_Encoding.is_active(buffer)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	310
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	311	def open_popup(result: Completion.Result)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	312	{
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	313	val font =
55825 694833e3e4a0 tuned signature -- separate module Font_Info; wenzelm parents: 55813 diff changeset	314	painter.getFont.deriveFont(
694833e3e4a0 tuned signature -- separate module Font_Info; wenzelm parents: 55813 diff changeset	315	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	316
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	317	val range = result.range
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	318
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	319	val loc1 = text_area.offsetToXY(range.start)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	320	if (loc1 != null) {
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	321	val loc2 =
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	322	SwingUtilities.convertPoint(painter,
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	323	loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	324
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	325	val items = result.items.map(new Item(_))
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	326	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	327	new Completion_Popup(Some(range), layered, loc2, font, items)
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	328	{
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	329	override def complete(item: Completion.Item) {
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	330	PIDE.completion_history.update(item)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	331	insert(item)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	332	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	333	override def propagate(evt: KeyEvent) {
56840 879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT); wenzelm parents: 56662 diff changeset	334	if (view.getKeyEventInterceptor == null)
879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT); wenzelm parents: 56662 diff changeset	335	JEdit_Lib.propagate_key(view, evt)
879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT); wenzelm parents: 56662 diff changeset	336	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	337	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	338	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	339	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	340	}
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	341	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	342	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	343	}
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	344	}
56171 15351577da10 clarified key event propagation, in accordance to outer_key_listener; wenzelm parents: 56170 diff changeset	345	if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	346	}
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	347	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	348	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	349	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	350	if (focus) text_area.requestFocus
56606 68b7a6db4a32 avoid ooddity: invoke intended function instead of java.awt.Container.invalidate(); wenzelm parents: 56605 diff changeset	351	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	352	}
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	353	}
57127 a406e15c3cf7 make double-sure that old popup is dismissed, before replacing it; wenzelm parents: 57051 diff changeset	354	dismissed()
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	355	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	356	view.setKeyEventInterceptor(completion.inner_key_listener)
56606 68b7a6db4a32 avoid ooddity: invoke intended function instead of java.awt.Container.invalidate(); wenzelm parents: 56605 diff changeset	357	JEdit_Lib.invalidate_range(text_area, range)
56841 bc6faeadbf82 reduced cluttering of popups; wenzelm parents: 56840 diff changeset	358	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	359	completion.show_popup(false)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	360	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	361	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	362
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	363	if (buffer.isEditable) {
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	364	val (no_completion, semantic_completion, opt_rendering) =
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	365	{
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	366	PIDE.document_view(text_area) match {
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	367	case Some(doc_view) =>
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	368	val rendering = doc_view.get_rendering()
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	369	val (no_completion, result) =
56593 0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	370	{
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	371	val caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	372	rendering.semantic_completion(caret_range) match {
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	373	case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	374	case Some(Text.Info(range, names: Completion.Names)) =>
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	375	val result =
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	376	JEdit_Lib.try_get_text(buffer, range) match {
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	377	case Some(original) => names.complete(range, history, decode, original)
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	378	case None => None
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	379	}
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	380	(false, result)
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	381	case None => (false, None)
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	382	}
56593 0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de); wenzelm parents: 56589 diff changeset	383	}
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	384	(no_completion, result, Some(rendering))
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	385	case None => (false, None, None)
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	386	}
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	387	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	388	if (no_completion) false
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	389	else {
56564 94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	390	val result =
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	391	{
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	392	val result0 =
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	393	if (word_only) None
5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	394	else
56587 83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	395	Completion.Result.merge(history, semantic_completion,
83777a91f5de clarified before_caret_range: prevent continuation on next line; wenzelm parents: 56586 diff changeset	396	syntax_completion(history, explicit, opt_rendering))
56564 94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	397	opt_rendering match {
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	398	case None => result0
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	399	case Some(rendering) =>
56843 b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	400	Completion.Result.merge(history, result0,
b2bfcd8cda80 support for path completion based on file-system content; wenzelm parents: 56842 diff changeset	401	Completion.Result.merge(history,
57051 5e30ffe79980 spell-checker completion is restricted to explicit mode, to avoid odd effects with immediate edits vs. delayed language context markup, and occasional delays due to dictionary lookup of many variants; wenzelm parents: 56877 diff changeset	402	spell_checker_completion(explicit, rendering), path_completion(rendering)))
56564 94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name; wenzelm parents: 56326 diff changeset	403	}
56586 5ef60881681d explicit menu action to complete word; wenzelm parents: 56576 diff changeset	404	}
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	405	result match {
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	406	case Some(result) =>
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	407	result.items match {
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	408	case List(item) if result.unique && item.immediate && immediate =>
79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	409	insert(item)
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	410	true
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	411	case _ :: _ if !delayed =>
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	412	open_popup(result)
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	413	false
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	414	case _ => false
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	415	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	416	case None => false
56175 79c29244b377 merge semantic and syntax completion; wenzelm parents: 56173 diff changeset	417	}
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	418	}
55752 43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	419	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	420	else false
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	421	}
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	422
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	423
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	424	/* input key events */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	425
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	426	def input(evt: KeyEvent)
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	427	{
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	428	GUI_Thread.require {}
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	429
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	430	if (PIDE.options.bool("jedit_completion")) {
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	431	if (!evt.isConsumed) {
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	432	dismissed()
53397 b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords; wenzelm parents: 53337 diff changeset	433	if (evt.getKeyChar != '\b') {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	434	val special = JEdit_Lib.special_key(evt)
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	435	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	436	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	437	input_delay.revoke()
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	438	action(immediate = immediate)
53397 b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords; wenzelm parents: 53337 diff changeset	439	}
56326 c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	440	else {
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	441	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	442	input_delay.revoke()
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	443	else
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	444	input_delay.invoke()
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549; wenzelm parents: 56325 diff changeset	445	}
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	446	}
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	447	}
53228 f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	448	}
f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	449	}
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	450
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	451	private val input_delay =
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	452	GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
53322 a4cd032172e0 allow short words for explicit completion; wenzelm parents: 53297 diff changeset	453	action()
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	454	}
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	455
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	456
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	457	/* dismiss popup */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	458
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	459	def dismissed(): Boolean =
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	460	{
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	461	GUI_Thread.require {}
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	462
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	463	completion_popup match {
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	464	case Some(completion) =>
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	465	completion.hide_popup()
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	466	completion_popup = None
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	467	true
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	468	case None =>
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	469	false
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	470	}
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	471	}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	472
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	473
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	474	/* activation */
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	475
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	476	private val outer_key_listener =
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	477	JEdit_Lib.key_listener(key_typed = input _)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	478
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	479	private def activate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	480	{
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	481	text_area.addKeyListener(outer_key_listener)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	482	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	483
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	484	private def deactivate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	485	{
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	486	dismissed()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	487	text_area.removeKeyListener(outer_key_listener)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	488	}
53228 f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	489	}
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	490
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	491
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	492
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	493	/ history text field /
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	494
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	495	class History_Text_Field(
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	496	name: String = null,
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	497	instant_popups: Boolean = false,
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	498	enter_adds_to_history: Boolean = true,
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	499	syntax: Outer_Syntax = Outer_Syntax.init) extends
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	500	HistoryTextField(name, instant_popups, enter_adds_to_history)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	501	{
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	502	text_field =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	503
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	504	// 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	505	if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	506
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	507	// owned by GUI thread
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	508	private var completion_popup: Option[Completion_Popup] = None
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	509
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	510
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	511	/* dismiss */
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	private def dismissed(): Boolean =
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	514	{
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	515	completion_popup match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	516	case Some(completion) =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	517	completion.hide_popup()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	518	completion_popup = None
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	519	true
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	520	case None =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	521	false
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	522	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	523	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	524
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	/* insert */
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	private def insert(item: Completion.Item)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	529	{
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	530	GUI_Thread.require {}
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	531
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	532	val range = item.range
56863 5fdb61a9a010 allow empty original, e.g. path ""; wenzelm parents: 56844 diff changeset	533	if (text_field.isEditable) {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	534	val content = text_field.getText
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	535	JEdit_Lib.try_get_text(content, range) match {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	536	case Some(text) if text == item.original =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	537	text_field.setText(
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	538	content.substring(0, range.start) +
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	539	item.replacement +
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	540	content.substring(range.stop))
19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	541	text_field.getCaret.setDot(range.start + item.replacement.length + item.move)
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	542	case _ =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	543	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	544	}
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
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	547
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	548	/* completion action: text field */
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	549
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	550	def action()
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	GUI.layered_pane(text_field) match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	553	case Some(layered) if text_field.isEditable =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	554	val history = PIDE.completion_history.value
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	555
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	556	val caret = text_field.getCaret.getDot
55813 08a1c860bc12 allow completion within a word (or symbol), like semantic completion; wenzelm parents: 55767 diff changeset	557	val text = text_field.getText
55748 2e1398b484aa no word completion within word context; wenzelm parents: 55747 diff changeset	558
55749 75a48dc4383e tuned signature; wenzelm parents: 55748 diff changeset	559	val context = syntax.language_context
55748 2e1398b484aa no word completion within word context; wenzelm parents: 55747 diff changeset	560
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	561	syntax.completion.complete(history, true, false, 0, text, caret, context) match {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	562	case Some(result) =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	563	val fm = text_field.getFontMetrics(text_field.getFont)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	564	val loc =
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	565	SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	566
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	567	val items = result.items.map(new Item(_))
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	568	val completion =
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	569	new Completion_Popup(None, layered, loc, text_field.getFont, items)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	570	{
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	571	override def complete(item: Completion.Item) {
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	572	PIDE.completion_history.update(item)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	573	insert(item)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	574	}
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	575	override def propagate(evt: KeyEvent) {
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	576	if (!evt.isConsumed) text_field.processKeyEvent(evt)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	577	}
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	override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus }
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	579	}
57127 a406e15c3cf7 make double-sure that old popup is dismissed, before replacing it; wenzelm parents: 57051 diff changeset	580	dismissed()
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	581	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	582	completion.show_popup(true)
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	583
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	584	case None =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	585	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	586	case _ =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	587	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	588	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	589
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	590
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	591	/* process key event */
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	592
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	593	private def process(evt: KeyEvent)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	594	{
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	595	if (PIDE.options.bool("jedit_completion")) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	596	dismissed()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	597	if (evt.getKeyChar != '\b') {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	598	val special = JEdit_Lib.special_key(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	599	if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	600	process_delay.revoke()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	601	action()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	602	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	603	else process_delay.invoke()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	604	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	605	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	606	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	607
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	608	private val process_delay =
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	609	GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	610	action()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	611	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	612
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	613	override def processKeyEvent(evt0: KeyEvent)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	614	{
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	615	val evt = KeyEventWorkaround.processKeyEvent(evt0)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	616	if (evt != null) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	617	evt.getID match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	618	case KeyEvent.KEY_PRESSED =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	619	val key_code = evt.getKeyCode
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	620	if (key_code == KeyEvent.VK_ESCAPE) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	621	if (dismissed()) evt.consume
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	622	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	623	case KeyEvent.KEY_TYPED =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	624	super.processKeyEvent(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	625	process(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	626	evt.consume
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	627	case _ =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	628	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	629	if (!evt.isConsumed) super.processKeyEvent(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	630	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	631	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	632	}
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	633	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	634
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	635
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	636	class Completion_Popup private(
56605 46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	637	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	638	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	639	location: Point,
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	640	font: Font,
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	641	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	642	{
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	643	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	644
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57588 diff changeset	645	GUI_Thread.require {}
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	646
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	647	require(!items.isEmpty)
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	648	val multi = items.length > 1
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	649
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	650
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	651	/* actions */
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	652
53275 b34aac6511ab tuned signature; wenzelm parents: 53274 diff changeset	653	def complete(item: Completion.Item) { }
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	654	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	655	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	656
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	657
f127e949389f Completion popup 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	/* 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	659
f127e949389f Completion popup 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	private val list_view = new ListView(items)
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	661	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	662	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	663	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	664	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	665	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	666
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	667	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	668	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	669	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	670	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	671
53023 f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	672	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	673	{
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	674	list_view.selection.items.toList match {
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	675	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	676	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	677	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	678	}
f127e949389f Completion popup 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	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	681	{
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	682	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	683	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	684	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	685	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	686	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	687	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	688	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	689
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	690	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	691	{
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	692	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	693	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	694	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	695
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	696
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	697	/* 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	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	val inner_key_listener =
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	700	JEdit_Lib.key_listener(
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	701	key_pressed = (e: KeyEvent) =>
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	702	{
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	703	if (!e.isConsumed) {
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	704	e.getKeyCode match {
57833 2c2bae3da1c2 completion popup supports both ENTER and TAB (default); wenzelm parents: 57612 diff changeset	705	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	706	if (complete_selected()) e.consume
2c2bae3da1c2 completion popup supports both ENTER and TAB (default); wenzelm parents: 57612 diff changeset	707	hide_popup()
2c2bae3da1c2 completion popup supports both ENTER and TAB (default); wenzelm parents: 57612 diff changeset	708	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	709	if (complete_selected()) e.consume
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	710	hide_popup()
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	711	case KeyEvent.VK_ESCAPE =>
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	712	hide_popup()
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	713	e.consume
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	714	case KeyEvent.VK_UP \| KeyEvent.VK_KP_UP if multi =>
53407 2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	715	move_items(-1)
2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	716	e.consume
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	717	case KeyEvent.VK_DOWN \| KeyEvent.VK_KP_DOWN if multi =>
53407 2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	718	move_items(1)
2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	719	e.consume
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	720	case KeyEvent.VK_PAGE_UP if multi =>
53407 2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	721	move_pages(-1)
2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	722	e.consume
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	723	case KeyEvent.VK_PAGE_DOWN if multi =>
53407 2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	724	move_pages(1)
2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	725	e.consume
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	726	case _ =>
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	727	if (e.isActionKey \|\| e.isAltDown \|\| e.isMetaDown \|\| e.isControlDown)
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	728	hide_popup()
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	729	}
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	730	}
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	731	propagate(e)
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	732	},
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	733	key_typed = propagate _
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	734	)
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	735
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	736	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	737
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	738	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	739	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	740	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	741	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	742	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	743	})
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	744
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	745	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	746	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	747	})
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	748
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	749
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	750	/* 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	751
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	752	override def getFocusTraversalKeysEnabled = false
53297 64c31de7f21c border as for Pretty_Tooltip; wenzelm parents: 53296 diff changeset	753	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	754	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	755
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	756
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	757	/* 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	758
56605 46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	759	def active_range: Option[Text.Range] =
46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	760	if (isDisplayable) opt_range else None
46313aafaf87 tuned; wenzelm parents: 56593 diff changeset	761
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	762	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	763	{
53247 bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations; wenzelm parents: 53246 diff changeset	764	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	765	val size =
53230 6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	766	{
6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	767	val geometry = JEdit_Lib.window_geometry(completion, completion)
6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	768	val bounds = Rendering.popup_bounds
53247 bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations; wenzelm parents: 53246 diff changeset	769	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	770	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	771	new Dimension(w, h)
53230 6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	772	}
53247 bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations; wenzelm parents: 53246 diff changeset	773	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	774	}
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	775
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	776	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	777	{
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	778	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	779	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	780	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	781
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	782	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	783	{
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	784	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	785	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	786	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	787	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	788

author	wenzelm
	Sat, 04 Oct 2014 18:05:30 +0200
changeset 58535	4815429974fe
parent 57833	2c2bae3da1c2
child 58549	d4d97b79f1fb
permissions	-rw-r--r--