author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73367 | 77ef8bef0593 |
child 76487 | 304ae1a6e160 |
permissions | -rw-r--r-- |
49702 | 1 |
/* Title: Tools/jEdit/src/pretty_tooltip.scala |
2 |
Author: Makarius |
|
3 |
||
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53230
diff
changeset
|
4 |
Tooltip based on Pretty_Text_Area. |
49702 | 5 |
*/ |
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
12 |
import java.awt.{Color, Point, BorderLayout, Dimension} |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
13 |
import java.awt.event.{FocusAdapter, FocusEvent} |
53778
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
14 |
import javax.swing.{JPanel, JComponent, SwingUtilities, JLayeredPane} |
49702 | 15 |
import javax.swing.border.LineBorder |
16 |
||
49725 | 17 |
import scala.swing.{FlowPanel, Label} |
18 |
import scala.swing.event.MouseClicked |
|
19 |
||
49702 | 20 |
import org.gjt.sp.jedit.View |
21 |
import org.gjt.sp.jedit.textarea.TextArea |
|
22 |
||
23 |
||
75393 | 24 |
object Pretty_Tooltip { |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
25 |
/* tooltip hierarchy */ |
51449
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
26 |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56930
diff
changeset
|
27 |
// owned by GUI thread |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
28 |
private var stack: List[Pretty_Tooltip] = Nil |
51449
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
29 |
|
75393 | 30 |
private def hierarchy( |
31 |
tip: Pretty_Tooltip |
|
32 |
): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] = { |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56930
diff
changeset
|
33 |
GUI_Thread.require {} |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
34 |
|
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
35 |
if (stack.contains(tip)) Some(stack.span(_ != tip)) |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
36 |
else None |
51449
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
37 |
} |
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
38 |
|
56497
0c63f3538639
dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
wenzelm
parents:
56341
diff
changeset
|
39 |
private def descendant(parent: JComponent): Option[Pretty_Tooltip] = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56930
diff
changeset
|
40 |
GUI_Thread.require { stack.find(tip => tip.original_parent == parent) } |
56497
0c63f3538639
dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
wenzelm
parents:
56341
diff
changeset
|
41 |
|
51449
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
42 |
def apply( |
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
43 |
view: View, |
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
44 |
parent: JComponent, |
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53230
diff
changeset
|
45 |
location: Point, |
64621 | 46 |
rendering: JEdit_Rendering, |
51449
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
47 |
results: Command.Results, |
75393 | 48 |
info: Text.Info[XML.Body] |
49 |
): Unit = { |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56930
diff
changeset
|
50 |
GUI_Thread.require {} |
51449
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
51 |
|
52497 | 52 |
stack match { |
53779 | 53 |
case top :: _ if top.results == results && top.info == info => |
52497 | 54 |
case _ => |
53778
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
55 |
GUI.layered_pane(parent) match { |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
56 |
case None => |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
57 |
case Some(layered) => |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
58 |
val (old, rest) = |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
59 |
GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match { |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
60 |
case Some(tip) => hierarchy(tip).getOrElse((stack, Nil)) |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
61 |
case None => (stack, Nil) |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
62 |
} |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
63 |
old.foreach(_.hide_popup) |
52497 | 64 |
|
53778
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
65 |
val loc = SwingUtilities.convertPoint(parent, location, layered) |
56497
0c63f3538639
dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
wenzelm
parents:
56341
diff
changeset
|
66 |
val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info) |
53778
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
67 |
stack = tip :: rest |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
68 |
tip.show_popup |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
69 |
} |
52496
8188e5286662
avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);
wenzelm
parents:
52494
diff
changeset
|
70 |
} |
51449
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
71 |
} |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
72 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
73 |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56930
diff
changeset
|
74 |
/* pending event and active state */ // owned by GUI thread |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
75 |
|
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
76 |
private var pending: Option[() => Unit] = None |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
77 |
private var active = true |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
78 |
|
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
79 |
private val pending_delay = |
71704 | 80 |
Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) { |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
81 |
pending match { |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
82 |
case Some(body) => pending = None; body() |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
83 |
case None => |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
84 |
} |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
85 |
} |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
86 |
|
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
87 |
def invoke(body: () => Unit): Unit = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56930
diff
changeset
|
88 |
GUI_Thread.require { |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
89 |
if (active) { |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
90 |
pending = Some(body) |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
91 |
pending_delay.invoke() |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
92 |
} |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
93 |
} |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
94 |
|
52664
e99a0a43720b
deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
wenzelm
parents:
52548
diff
changeset
|
95 |
def revoke(): Unit = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56930
diff
changeset
|
96 |
GUI_Thread.require { |
52664
e99a0a43720b
deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
wenzelm
parents:
52548
diff
changeset
|
97 |
pending = None |
e99a0a43720b
deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
wenzelm
parents:
52548
diff
changeset
|
98 |
pending_delay.revoke() |
e99a0a43720b
deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
wenzelm
parents:
52548
diff
changeset
|
99 |
} |
e99a0a43720b
deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
wenzelm
parents:
52548
diff
changeset
|
100 |
|
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
101 |
private lazy val reactivate_delay = |
71704 | 102 |
Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) { |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
103 |
active = true |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
104 |
} |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
105 |
|
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
106 |
private def deactivate(): Unit = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56930
diff
changeset
|
107 |
GUI_Thread.require { |
52664
e99a0a43720b
deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
wenzelm
parents:
52548
diff
changeset
|
108 |
revoke() |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
109 |
active = false |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
110 |
reactivate_delay.invoke() |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
111 |
} |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
112 |
|
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
113 |
|
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
114 |
/* dismiss */ |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
115 |
|
75393 | 116 |
private lazy val focus_delay = |
117 |
Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { |
|
118 |
dismiss_unfocused() |
|
119 |
} |
|
56341
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
120 |
|
75393 | 121 |
def dismiss_unfocused(): Unit = { |
56341
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
122 |
stack.span(tip => !tip.pretty_text_area.isFocusOwner) match { |
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
123 |
case (Nil, _) => |
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
124 |
case (unfocused, rest) => |
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
125 |
deactivate() |
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
126 |
unfocused.foreach(_.hide_popup) |
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
127 |
stack = rest |
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
128 |
} |
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
129 |
} |
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
130 |
|
75393 | 131 |
def dismiss(tip: Pretty_Tooltip): Unit = { |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
132 |
deactivate() |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
133 |
hierarchy(tip) match { |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
134 |
case Some((old, _ :: rest)) => |
52498 | 135 |
rest match { |
136 |
case top :: _ => top.request_focus |
|
66592 | 137 |
case Nil => JEdit_Lib.request_focus_view() |
52498 | 138 |
} |
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:
53779
diff
changeset
|
139 |
old.foreach(_.hide_popup) |
3eb84b6b0353
transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;
wenzelm
parents:
53779
diff
changeset
|
140 |
tip.hide_popup |
3eb84b6b0353
transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;
wenzelm
parents:
53779
diff
changeset
|
141 |
stack = rest |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
142 |
case _ => |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
143 |
} |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
144 |
} |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
145 |
|
56497
0c63f3538639
dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
wenzelm
parents:
56341
diff
changeset
|
146 |
def dismiss_descendant(parent: JComponent): Unit = |
71601 | 147 |
descendant(parent).foreach(dismiss) |
56497
0c63f3538639
dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
wenzelm
parents:
56341
diff
changeset
|
148 |
|
75393 | 149 |
def dismissed_all(): Boolean = { |
52664
e99a0a43720b
deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
wenzelm
parents:
52548
diff
changeset
|
150 |
deactivate() |
52548
a1a8248a4677
some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
wenzelm
parents:
52498
diff
changeset
|
151 |
if (stack.isEmpty) false |
a1a8248a4677
some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
wenzelm
parents:
52498
diff
changeset
|
152 |
else { |
66592 | 153 |
JEdit_Lib.request_focus_view() |
52548
a1a8248a4677
some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
wenzelm
parents:
52498
diff
changeset
|
154 |
stack.foreach(_.hide_popup) |
a1a8248a4677
some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
wenzelm
parents:
52498
diff
changeset
|
155 |
stack = Nil |
a1a8248a4677
some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
wenzelm
parents:
52498
diff
changeset
|
156 |
true |
a1a8248a4677
some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
wenzelm
parents:
52498
diff
changeset
|
157 |
} |
52664
e99a0a43720b
deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
wenzelm
parents:
52548
diff
changeset
|
158 |
} |
51449
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
159 |
} |
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
160 |
|
8d6e478934dc
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
wenzelm
parents:
51440
diff
changeset
|
161 |
|
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
162 |
class Pretty_Tooltip private( |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
163 |
view: View, |
53778
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53712
diff
changeset
|
164 |
layered: JLayeredPane, |
56497
0c63f3538639
dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
wenzelm
parents:
56341
diff
changeset
|
165 |
val original_parent: JComponent, |
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53230
diff
changeset
|
166 |
location: Point, |
64621 | 167 |
rendering: JEdit_Rendering, |
52496
8188e5286662
avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);
wenzelm
parents:
52494
diff
changeset
|
168 |
private val results: Command.Results, |
75393 | 169 |
private val info: Text.Info[XML.Body] |
170 |
) extends JPanel(new BorderLayout) { |
|
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
171 |
tip => |
49705 | 172 |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56930
diff
changeset
|
173 |
GUI_Thread.require {} |
49725 | 174 |
|
175 |
||
176 |
/* controls */ |
|
177 |
||
49727 | 178 |
private val close = new Label { |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
179 |
icon = rendering.tooltip_close_icon |
49727 | 180 |
tooltip = "Close tooltip window" |
181 |
listenTo(mouse.clicks) |
|
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
182 |
reactions += { case _: MouseClicked => Pretty_Tooltip.dismiss(tip) } |
49727 | 183 |
} |
184 |
||
49726 | 185 |
private val detach = new Label { |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
186 |
icon = rendering.tooltip_detach_icon |
49726 | 187 |
tooltip = "Detach tooltip window" |
188 |
listenTo(mouse.clicks) |
|
189 |
reactions += { |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50206
diff
changeset
|
190 |
case _: MouseClicked => |
52496
8188e5286662
avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);
wenzelm
parents:
52494
diff
changeset
|
191 |
Info_Dockable(view, rendering.snapshot, results, info.info) |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
192 |
Pretty_Tooltip.dismiss(tip) |
49726 | 193 |
} |
194 |
} |
|
195 |
||
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
196 |
private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) { |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
197 |
background = rendering.tooltip_color |
49709 | 198 |
} |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
199 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
200 |
|
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
201 |
/* text area */ |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
202 |
|
71601 | 203 |
val pretty_text_area: Pretty_Text_Area = |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
204 |
new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) { |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
205 |
override def get_background() = Some(rendering.tooltip_color) |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
206 |
} |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
207 |
|
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
208 |
pretty_text_area.addFocusListener(new FocusAdapter { |
75393 | 209 |
override def focusGained(e: FocusEvent): Unit = { |
52493 | 210 |
tip_border(true) |
56341
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
211 |
Pretty_Tooltip.focus_delay.invoke() |
52491
d435febab327
visually explicit focus (behaviour dependent on platform and look-and-feel);
wenzelm
parents:
52484
diff
changeset
|
212 |
} |
75393 | 213 |
override def focusLost(e: FocusEvent): Unit = { |
56341
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
214 |
tip_border(false) |
bfd13102eb54
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
wenzelm
parents:
55825
diff
changeset
|
215 |
Pretty_Tooltip.focus_delay.invoke() |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
216 |
} |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
217 |
}) |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
218 |
|
55825 | 219 |
pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_popup_font_scale"))) |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
220 |
|
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
221 |
|
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
222 |
/* main content */ |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
223 |
|
75393 | 224 |
def tip_border(has_focus: Boolean): Unit = { |
52493 | 225 |
tip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY)) |
52491
d435febab327
visually explicit focus (behaviour dependent on platform and look-and-feel);
wenzelm
parents:
52484
diff
changeset
|
226 |
tip.repaint() |
d435febab327
visually explicit focus (behaviour dependent on platform and look-and-feel);
wenzelm
parents:
52484
diff
changeset
|
227 |
} |
52493 | 228 |
tip_border(true) |
52491
d435febab327
visually explicit focus (behaviour dependent on platform and look-and-feel);
wenzelm
parents:
52484
diff
changeset
|
229 |
|
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
230 |
override def getFocusTraversalKeysEnabled = false |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
231 |
tip.setBackground(rendering.tooltip_color) |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
232 |
tip.add(controls.peer, BorderLayout.NORTH) |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
233 |
tip.add(pretty_text_area) |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
234 |
|
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
235 |
|
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
236 |
/* popup */ |
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
237 |
|
75393 | 238 |
private val popup = { |
72974 | 239 |
val screen = GUI.screen_location(layered, location) |
75393 | 240 |
val size = { |
64621 | 241 |
val bounds = JEdit_Rendering.popup_bounds |
57849 | 242 |
|
243 |
val w_max = layered.getWidth min (screen.bounds.width * bounds).toInt |
|
244 |
val h_max = layered.getHeight min (screen.bounds.height * bounds).toInt |
|
245 |
||
52492 | 246 |
val painter = pretty_text_area.getPainter |
57849 | 247 |
val geometry = JEdit_Lib.window_geometry(tip, painter) |
52492 | 248 |
val metric = JEdit_Lib.pretty_metric(painter) |
57849 | 249 |
|
250 |
val margin = |
|
251 |
((rendering.tooltip_margin * metric.average) min |
|
252 |
((w_max - geometry.deco_width) / metric.unit).toInt) max 20 |
|
52492 | 253 |
|
67547
aefe7a7b330a
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
wenzelm
parents:
67546
diff
changeset
|
254 |
val formatted = Pretty.formatted(info.info, margin = margin, metric = metric) |
52492 | 255 |
val lines = |
67546 | 256 |
XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)( |
71601 | 257 |
(n: Int, s: String) => n + s.iterator.count(_ == '\n')) |
52492 | 258 |
|
67546 | 259 |
val h = painter.getLineHeight * lines + geometry.deco_height |
52492 | 260 |
val margin1 = |
73358 | 261 |
if (h <= h_max) { |
73359 | 262 |
split_lines(XML.content(formatted)).foldLeft(0.0) { case (m, line) => m max metric(line) } |
73358 | 263 |
} |
52492 | 264 |
else margin |
57849 | 265 |
val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width |
53184
5d6ffb87ee08
confine popup to parent component, to avoid javax.swing.PopupFactory$HeavyWeightPopup and its problems with Linux window management and Mac OS X key handling;
wenzelm
parents:
53019
diff
changeset
|
266 |
|
57849 | 267 |
new Dimension(w min w_max, h min h_max) |
52492 | 268 |
} |
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53230
diff
changeset
|
269 |
new Popup(layered, tip, screen.relative(layered, size), size) |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
270 |
} |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
271 |
|
75393 | 272 |
private def show_popup: Unit = { |
52484
23a09c639700
avoid potential race condition of focusLost/dismiss vs. popup.show;
wenzelm
parents:
52483
diff
changeset
|
273 |
popup.show |
73367 | 274 |
pretty_text_area.requestFocus() |
52496
8188e5286662
avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);
wenzelm
parents:
52494
diff
changeset
|
275 |
pretty_text_area.update(rendering.snapshot, results, info.info) |
52484
23a09c639700
avoid potential race condition of focusLost/dismiss vs. popup.show;
wenzelm
parents:
52483
diff
changeset
|
276 |
} |
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
277 |
|
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
52472
diff
changeset
|
278 |
private def hide_popup: Unit = popup.hide |
52498 | 279 |
|
73367 | 280 |
private def request_focus: Unit = pretty_text_area.requestFocus() |
49702 | 281 |
} |
282 |