isabelle: src/Tools/jEdit/src/completion_popup.scala@638b29331549 (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}
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	14	import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
53297 64c31de7f21c border as for Pretty_Tooltip; wenzelm parents: 53296 diff changeset	15	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	16	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	17
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	18	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	19	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	20
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	21	import org.gjt.sp.jedit.View
55712 e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	22	import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	23	import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
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	24
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	25
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	26	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	27	{
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	28	/ items with HTML rendering /
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	29
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	30	private class Item(val item: Completion.Item)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	31	{
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	32	private val html =
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	33	item.description match {
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	34	case a :: bs =>
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	35	"<html><b>" + HTML.encode(a) + "</b>" +
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	36	HTML.encode(bs.map(" " + _).mkString) + "</html>"
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	37	case Nil => ""
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	38	}
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	39	override def toString: String = html
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	40	}
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	41
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	42
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	43
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	44	/ 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	45
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	46	object Text_Area
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	47	{
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	48	private val key = new Object
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	49
55712 e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	50	def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	51	{
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	52	Swing_Thread.require()
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	53	text_area.getClientProperty(key) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	54	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	55	case _ => None
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	56	}
55712 e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	57	}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	58
55712 e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	59	def active_range(text_area: TextArea): Option[Text.Range] =
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	60	apply(text_area) match {
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	61	case Some(text_area_completion) => text_area_completion.active_range
e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	62	case None => None
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	63	}
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	64
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	65	def action(text_area: TextArea): Boolean =
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	66	apply(text_area) match {
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	67	case Some(text_area_completion) =>
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	68	if (text_area_completion.active_range.isDefined)
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	69	text_area_completion.action(immediate = true, explicit = true)
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	70	else text_area_completion.action()
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	71	true
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	72	case None => false
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	73	}
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	74
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	75	def exit(text_area: JEditTextArea)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	76	{
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	77	Swing_Thread.require()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	78	apply(text_area) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	79	case None =>
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	80	case Some(text_area_completion) =>
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	81	text_area_completion.deactivate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	82	text_area.putClientProperty(key, null)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	83	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	84	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	85
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	86	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	87	{
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	88	exit(text_area)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	89	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	90	text_area.putClientProperty(key, text_area_completion)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	91	text_area_completion.activate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	92	text_area_completion
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	93	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	94
55712 e757e8c8d8ea tuned signature -- weaker type requirement; wenzelm parents: 55711 diff changeset	95	def dismissed(text_area: TextArea): Boolean =
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	96	{
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	97	Swing_Thread.require()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	98	apply(text_area) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	99	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	100	case None => false
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	101	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	102	}
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	103	}
0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	104
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	105	class Text_Area private(text_area: JEditTextArea)
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	106	{
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	107	// owned by Swing thread
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	108	private var completion_popup: Option[Completion_Popup] = None
0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	109
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	110	def active_range: Option[Text.Range] =
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	111	completion_popup match {
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	112	case Some(completion) =>
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	113	completion.active_range match {
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	114	case Some((range, _)) if completion.isDisplayable => Some(range)
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	115	case _ => None
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	116	}
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	117	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
55767 96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	121	/* caret */
96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	122
96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	123	def before_caret_range(rendering: Rendering): Text.Range =
96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	124	{
96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	125	val snapshot = rendering.snapshot
96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	126	val former_caret = snapshot.revert(text_area.getCaretPosition)
96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	127	snapshot.convert(Text.Range(former_caret - 1, former_caret))
96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	128	}
96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	129
96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	130
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	131	/* rendering */
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	132
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	133	def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	134	{
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	135	active_range match {
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	136	case Some(range) => range.try_restrict(line_range)
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	137	case None =>
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	138	val buffer = text_area.getBuffer
55767 96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	139	if (line_range.contains(text_area.getCaretPosition)) {
96ddf9bf12ac more precise before_caret_range (looking both in space and time); wenzelm parents: 55752 diff changeset	140	before_caret_range(rendering).try_restrict(line_range) match {
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	141	case Some(range) if !range.is_singularity =>
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	142	rendering.completion_names(range) match {
55914 c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset; wenzelm parents: 55850 diff changeset	143	case Some(names) =>
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset; wenzelm parents: 55850 diff changeset	144	if (names.no_completion) None
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset; wenzelm parents: 55850 diff changeset	145	else Some(names.range)
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	146	case None =>
55752 43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	147	syntax_completion(false, Some(rendering)) match {
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	148	case Some(result) => Some(result.range)
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	149	case None => None
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	150	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	151	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	152	case _ => None
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	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	155	else None
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	}.map(range => Text.Info(range, rendering.completion_color))
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	158
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	159
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	160	/* syntax completion */
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	161
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	162	def syntax_completion(
55752 43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	163	explicit: Boolean, opt_rendering: Option[Rendering] = None): Option[Completion.Result] =
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	164	{
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	165	val buffer = text_area.getBuffer
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	166	val history = PIDE.completion_history.value
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	167	val decode = Isabelle_Encoding.is_active(buffer)
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	168
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	169	Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	170	case Some(syntax) =>
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	171	val caret = text_area.getCaretPosition
55813 08a1c860bc12 allow completion within a word (or symbol), like semantic completion; wenzelm parents: 55767 diff changeset	172
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	173	val line = buffer.getLineOfOffset(caret)
55813 08a1c860bc12 allow completion within a word (or symbol), like semantic completion; wenzelm parents: 55767 diff changeset	174	val line_start = buffer.getLineStartOffset(line)
08a1c860bc12 allow completion within a word (or symbol), like semantic completion; wenzelm parents: 55767 diff changeset	175	val line_length = (buffer.getLineEndOffset(line) min buffer.getLength) - line_start
08a1c860bc12 allow completion within a word (or symbol), like semantic completion; wenzelm parents: 55767 diff changeset	176	val line_text = buffer.getSegment(line_start, line_length)
55748 2e1398b484aa no word completion within word context; wenzelm parents: 55747 diff changeset	177
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	178	val context =
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	179	(opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	180	case Some(rendering) =>
55828 42ac3cfb89f6 clarified language markup: added "delimited" property; wenzelm parents: 55825 diff changeset	181	rendering.completion_language(before_caret_range(rendering))
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	182	case None => None
55749 75a48dc4383e tuned signature; wenzelm parents: 55748 diff changeset	183	}) getOrElse syntax.language_context
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	184
55813 08a1c860bc12 allow completion within a word (or symbol), like semantic completion; wenzelm parents: 55767 diff changeset	185	syntax.completion.complete(
55850 7f229b0212fe no extend_word for now, it is in conflict with manual reformatting of sources via TAB (e.g. accidental replacement of 'assume' by 'assumes'); wenzelm parents: 55828 diff changeset	186	history, decode, explicit, line_start, line_text, caret - line_start, false, context)
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	187
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	188	case None => None
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	189	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	190	}
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	191
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	192
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	193	/* completion action: text area */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	194
53275 b34aac6511ab tuned signature; wenzelm parents: 53274 diff changeset	195	private def insert(item: Completion.Item)
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	196	{
142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	197	Swing_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	198
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	199	val buffer = text_area.getBuffer
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	200	val range = item.range
19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	201	if (buffer.isEditable && range.length > 0) {
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	202	JEdit_Lib.buffer_edit(buffer) {
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	203	JEdit_Lib.try_get_text(buffer, range) match {
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	204	case Some(text) if text == item.original =>
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	205	buffer.remove(range.start, range.length)
19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	206	buffer.insert(range.start, item.replacement)
19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	207	text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	208	case _ =>
142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	209	}
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	210	}
4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	211	}
4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	212	}
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	213
53322 a4cd032172e0 allow short words for explicit completion; wenzelm parents: 53297 diff changeset	214	def action(immediate: Boolean = false, explicit: Boolean = false)
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	215	{
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	216	val view = text_area.getView
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	217	val layered = view.getLayeredPane
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	218	val buffer = text_area.getBuffer
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	219	val painter = text_area.getPainter
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	220
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	221	val history = PIDE.completion_history.value
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	222	val decode = Isabelle_Encoding.is_active(buffer)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	223
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	224	def open_popup(result: Completion.Result)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	225	{
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	226	val font =
55825 694833e3e4a0 tuned signature -- separate module Font_Info; wenzelm parents: 55813 diff changeset	227	painter.getFont.deriveFont(
694833e3e4a0 tuned signature -- separate module Font_Info; wenzelm parents: 55813 diff changeset	228	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	229
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	230	val range = result.range
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	231	def invalidate(): Unit = JEdit_Lib.invalidate_range(text_area, range)
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	232
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	233	val loc1 = text_area.offsetToXY(range.start)
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	234	if (loc1 != null) {
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	235	val loc2 =
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	236	SwingUtilities.convertPoint(painter,
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	237	loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	238
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	239	val items = result.items.map(new Item(_))
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	240	val completion =
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	241	new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, items)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	242	{
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	243	override def complete(item: Completion.Item) {
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	244	PIDE.completion_history.update(item)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	245	insert(item)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	246	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	247	override def propagate(evt: KeyEvent) {
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	248	JEdit_Lib.propagate_key(view, evt)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	249	input(evt)
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	250	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	251	override def refocus() { text_area.requestFocus }
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	252	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	253	completion_popup = Some(completion)
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	254	invalidate()
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	255	completion.show_popup()
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	256	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	257	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	258
55752 43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	259	def semantic_completion(): Option[Completion.Result] =
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	260	PIDE.document_view(text_area) match {
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	261	case Some(doc_view) =>
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	262	val rendering = doc_view.get_rendering()
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	263	rendering.completion_names(before_caret_range(rendering)) match {
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	264	case Some(names) =>
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	265	if (names.no_completion)
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	266	Some(Completion.Result.empty(names.range))
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	267	else
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	268	JEdit_Lib.try_get_text(buffer, names.range) match {
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	269	case Some(original) => names.complete(history, decode, original)
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	270	case None => None
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	271	}
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	272	case None => None
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	273	}
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	274	case None => None
55693 93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	275	}
93ba0085e888 try explicit semantic completion before syntax completion; wenzelm parents: 55692 diff changeset	276
55752 43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	277	if (buffer.isEditable) {
43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	278	semantic_completion() orElse syntax_completion(explicit) match {
55747 bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	279	case Some(result) =>
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	280	result.items match {
bef19c929ba5 more completion rendering: active, semantic, syntactic; wenzelm parents: 55712 diff changeset	281	case List(item) if result.unique && item.immediate && immediate =>
55752 43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	282	insert(item)
43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	283	case _ :: _ =>
43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	284	open_popup(result)
43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	285	case _ =>
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	286	}
55752 43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	287	case None =>
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	288	}
55752 43d0e2a34c9d uniform insert vs. popup policy; wenzelm parents: 55749 diff changeset	289	}
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	290	}
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	291
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	292
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	293	/* input key events */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	294
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	295	def input(evt: KeyEvent)
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	296	{
142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	297	Swing_Thread.require()
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	298
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	299	if (PIDE.options.bool("jedit_completion")) {
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	300	if (!evt.isConsumed) {
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	301	dismissed()
53397 b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords; wenzelm parents: 53337 diff changeset	302	if (evt.getKeyChar != '\b') {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	303	val special = JEdit_Lib.special_key(evt)
53397 b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords; wenzelm parents: 53337 diff changeset	304	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	305	input_delay.revoke()
b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords; wenzelm parents: 53337 diff changeset	306	action(immediate = PIDE.options.bool("jedit_completion_immediate"))
b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords; wenzelm parents: 53337 diff changeset	307	}
b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords; wenzelm parents: 53337 diff changeset	308	else input_delay.invoke()
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	309	}
53242 142f4fff4e40 tuned signature; wenzelm parents: 53237 diff changeset	310	}
53228 f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	311	}
f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	312	}
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	313
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	314	private val input_delay =
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	315	Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
53322 a4cd032172e0 allow short words for explicit completion; wenzelm parents: 53297 diff changeset	316	action()
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	317	}
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	318
473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	319
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	320	/* dismiss popup */
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	321
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	322	def dismissed(): Boolean =
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	323	{
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	324	Swing_Thread.require()
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	325
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	326	completion_popup match {
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	327	case Some(completion) =>
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	328	completion.hide_popup()
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	329	completion_popup = None
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	330	true
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	331	case None =>
f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	332	false
53273 473ea1ed7503 some completion options; wenzelm parents: 53272 diff changeset	333	}
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 53275 diff changeset	334	}
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	335
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	336
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	337	/* activation */
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	338
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	339	private val outer_key_listener =
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	340	JEdit_Lib.key_listener(key_typed = input _)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	341
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	342	private def activate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	343	{
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	344	text_area.addKeyListener(outer_key_listener)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	345	}
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	346
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	347	private def deactivate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	348	{
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	349	dismissed()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	350	text_area.removeKeyListener(outer_key_listener)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	351	}
53228 f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup; wenzelm parents: 53226 diff changeset	352	}
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	353
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	354
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	355
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	356	/ history text field /
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	357
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	358	class History_Text_Field(
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	359	name: String = null,
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	360	instant_popups: Boolean = false,
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	361	enter_adds_to_history: Boolean = true,
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	362	syntax: Outer_Syntax = Outer_Syntax.init) extends
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	363	HistoryTextField(name, instant_popups, enter_adds_to_history)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	364	{
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	365	text_field =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	366
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	367	// 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	368	if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	369
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	370	// owned by Swing thread
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	371	private var completion_popup: Option[Completion_Popup] = None
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	372
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	373
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	374	/* dismiss */
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	375
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	376	private def dismissed(): Boolean =
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	377	{
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	378	completion_popup match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	379	case Some(completion) =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	380	completion.hide_popup()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	381	completion_popup = None
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	382	true
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	383	case None =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	384	false
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	385	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	386	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	387
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	388
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	389	/* insert */
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	390
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	391	private def insert(item: Completion.Item)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	392	{
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	393	Swing_Thread.require()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	394
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	395	val range = item.range
19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	396	if (text_field.isEditable && range.length > 0) {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	397	val content = text_field.getText
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	398	JEdit_Lib.try_get_text(content, range) match {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	399	case Some(text) if text == item.original =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	400	text_field.setText(
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	401	content.substring(0, range.start) +
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	402	item.replacement +
55692 19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	403	content.substring(range.stop))
19e8b00684f7 more explicit Completion.Item.range, independently of caret; wenzelm parents: 55690 diff changeset	404	text_field.getCaret.setDot(range.start + item.replacement.length + item.move)
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	405	case _ =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	406	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	407	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	408	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	409
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	410
56170 638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time; wenzelm parents: 55978 diff changeset	411	/* completion action: text field */
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	412
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	413	def action()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	414	{
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	415	GUI.layered_pane(text_field) match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	416	case Some(layered) if text_field.isEditable =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	417	val history = PIDE.completion_history.value
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	418
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	419	val caret = text_field.getCaret.getDot
55813 08a1c860bc12 allow completion within a word (or symbol), like semantic completion; wenzelm parents: 55767 diff changeset	420	val text = text_field.getText
55748 2e1398b484aa no word completion within word context; wenzelm parents: 55747 diff changeset	421
55749 75a48dc4383e tuned signature; wenzelm parents: 55748 diff changeset	422	val context = syntax.language_context
55748 2e1398b484aa no word completion within word context; wenzelm parents: 55747 diff changeset	423
55813 08a1c860bc12 allow completion within a word (or symbol), like semantic completion; wenzelm parents: 55767 diff changeset	424	syntax.completion.complete(history, true, false, 0, text, caret, false, context) match {
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	425	case Some(result) =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	426	val fm = text_field.getFontMetrics(text_field.getFont)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	427	val loc =
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	428	SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	429
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	430	val items = result.items.map(new Item(_))
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	431	val completion =
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	432	new Completion_Popup(None, layered, loc, text_field.getFont, items)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	433	{
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	434	override def complete(item: Completion.Item) {
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	435	PIDE.completion_history.update(item)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	436	insert(item)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	437	}
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	438	override def propagate(evt: KeyEvent) {
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	439	if (!evt.isConsumed) text_field.processKeyEvent(evt)
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	440	}
56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	441	override def refocus() { text_field.requestFocus }
53784 322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	442	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	443	completion_popup = Some(completion)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	444	completion.show_popup()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	445
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	446	case None =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	447	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	448	case _ =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	449	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	450	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	451
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	452
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	453	/* process key event */
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	454
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	455	private def process(evt: KeyEvent)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	456	{
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	457	if (PIDE.options.bool("jedit_completion")) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	458	dismissed()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	459	if (evt.getKeyChar != '\b') {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	460	val special = JEdit_Lib.special_key(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	461	if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	462	process_delay.revoke()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	463	action()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	464	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	465	else process_delay.invoke()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	466	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	467	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	468	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	469
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	470	private val process_delay =
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	471	Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	472	action()
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	473	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	474
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	475	override def processKeyEvent(evt0: KeyEvent)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	476	{
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	477	val evt = KeyEventWorkaround.processKeyEvent(evt0)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	478	if (evt != null) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	479	evt.getID match {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	480	case KeyEvent.KEY_PRESSED =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	481	val key_code = evt.getKeyCode
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	482	if (key_code == KeyEvent.VK_ESCAPE) {
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	483	if (dismissed()) evt.consume
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	484	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	485	case KeyEvent.KEY_TYPED =>
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	486	super.processKeyEvent(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	487	process(evt)
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	488	evt.consume
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	489	case _ =>
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	if (!evt.isConsumed) super.processKeyEvent(evt)
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	}
322a3ff42b33 completion popup for history text field; wenzelm parents: 53407 diff changeset	494	}
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	495	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	496
53233 4b422e5d64fd some actual completion via outer syntax; wenzelm parents: 53232 diff changeset	497
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	498	class Completion_Popup private(
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	499	val active_range: Option[(Text.Range, () => Unit)],
53246 8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); wenzelm parents: 53244 diff changeset	500	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	501	location: Point,
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	502	font: Font,
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	503	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	504	{
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	505	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	506
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	507	Swing_Thread.require()
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	508
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	509	require(!items.isEmpty)
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	510	val multi = items.length > 1
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	511
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	512
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	513	/* actions */
4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	514
53275 b34aac6511ab tuned signature; wenzelm parents: 53274 diff changeset	515	def complete(item: Completion.Item) { }
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	516	def propagate(evt: KeyEvent) { }
53234 ea4abbbe1702 more careful refocus operation: do not reset focus if it was already lost (relevant when activating a different GUI component, for example); wenzelm parents: 53233 diff changeset	517	def refocus() { }
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	518
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	519
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	520	/* 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	521
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	522	private val list_view = new ListView(items)
53272 0dfd78ff7696 more abstract Completion_Popup.Text_Area; wenzelm parents: 53247 diff changeset	523	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	524	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	525	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	526	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	527	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	528
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	529	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	530	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	531	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	532	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	533
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	534	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	535	{
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	536	list_view.selection.items.toList match {
55978 56645c447ee9 tuned description and its rendering; wenzelm parents: 55914 diff changeset	537	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	538	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	539	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	540	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	541
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	542	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	543	{
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	544	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	545	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	546	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	547	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	548	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	549	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	550	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	551
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	552	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	553	{
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	554	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	555	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	556	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	557
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	558
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	559	/* 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	560
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	561	private val inner_key_listener =
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	562	JEdit_Lib.key_listener(
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	563	key_pressed = (e: KeyEvent) =>
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	564	{
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	565	if (!e.isConsumed) {
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	566	e.getKeyCode match {
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	567	case KeyEvent.VK_TAB =>
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	568	if (complete_selected()) e.consume
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	569	hide_popup()
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	570	case KeyEvent.VK_ESCAPE =>
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	571	hide_popup()
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	572	e.consume
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	573	case KeyEvent.VK_UP \| KeyEvent.VK_KP_UP if multi =>
53407 2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	574	move_items(-1)
2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	575	e.consume
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	576	case KeyEvent.VK_DOWN \| KeyEvent.VK_KP_DOWN if multi =>
53407 2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	577	move_items(1)
2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	578	e.consume
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	579	case KeyEvent.VK_PAGE_UP if multi =>
53407 2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	580	move_pages(-1)
2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	581	e.consume
53405 ed2b48af04d9 interpret keys more movement only when needed; wenzelm parents: 53398 diff changeset	582	case KeyEvent.VK_PAGE_DOWN if multi =>
53407 2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	583	move_pages(1)
2add7d4c85bd tuned; wenzelm parents: 53405 diff changeset	584	e.consume
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	585	case _ =>
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	586	if (e.isActionKey \|\| e.isAltDown \|\| e.isMetaDown \|\| e.isControlDown)
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	587	hide_popup()
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	588	}
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	589	}
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	590	propagate(e)
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	591	},
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	592	key_typed = propagate _
53226 9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; wenzelm parents: 53023 diff changeset	593	)
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	594
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53273 diff changeset	595	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	596
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	597	list_view.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	598	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	599	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	600	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	601	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	602	})
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	603
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	604	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	605	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	606	})
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	607
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	608
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	609	/* 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	610
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	611	override def getFocusTraversalKeysEnabled = false
53297 64c31de7f21c border as for Pretty_Tooltip; wenzelm parents: 53296 diff changeset	612	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	613	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	614
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	615
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	616	/* 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	617
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	618	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	619	{
53247 bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations; wenzelm parents: 53246 diff changeset	620	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	621	val size =
53230 6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	622	{
6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	623	val geometry = JEdit_Lib.window_geometry(completion, completion)
6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	624	val bounds = Rendering.popup_bounds
53247 bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations; wenzelm parents: 53246 diff changeset	625	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	626	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	627	new Dimension(w, h)
53230 6589ff56cc3c determine completion geometry like tooltip; wenzelm parents: 53229 diff changeset	628	}
53247 bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations; wenzelm parents: 53246 diff changeset	629	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	630	}
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	631
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	632	private def show_popup()
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	633	{
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	634	popup.show
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	635	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	636	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	637
54377 750561986828 added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior); wenzelm parents: 54376 diff changeset	638	private val hide_popup_delay =
750561986828 added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior); wenzelm parents: 54376 diff changeset	639	Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) {
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	640	active_range match { case Some((_, invalidate)) => invalidate() case _ => }
54377 750561986828 added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior); wenzelm parents: 54376 diff changeset	641	popup.hide
750561986828 added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior); wenzelm parents: 54376 diff changeset	642	}
750561986828 added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior); wenzelm parents: 54376 diff changeset	643
53232 4a3762693452 tuned signature; wenzelm parents: 53231 diff changeset	644	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	645	{
54376 3eb84b6b0353 transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows; wenzelm parents: 53987 diff changeset	646	if (list_view.peer.isFocusOwner) refocus()
54377 750561986828 added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior); wenzelm parents: 54376 diff changeset	647
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	648	if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero) {
9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	649	active_range match { case Some((_, invalidate)) => invalidate() case _ => }
54377 750561986828 added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior); wenzelm parents: 54376 diff changeset	650	popup.hide
55711 9e3d64e5919a paint completion range of active popup; wenzelm parents: 55693 diff changeset	651	}
54377 750561986828 added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior); wenzelm parents: 54376 diff changeset	652	else hide_popup_delay.invoke()
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	653	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	654	}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); wenzelm parents: diff changeset	655

author	wenzelm
	Mon, 17 Mar 2014 10:45:29 +0100
changeset 56170	638b29331549
parent 55978	56645c447ee9
child 56171	15351577da10
permissions	-rw-r--r--