author | wenzelm |
Mon, 01 Jul 2013 14:30:56 +0200 | |
changeset 52494 | a1e09340c0f4 |
parent 52493 | ee7218d28159 |
child 52496 | 8188e5286662 |
permissions | -rw-r--r-- |
49702 | 1 |
/* Title: Tools/jEdit/src/pretty_tooltip.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Enhanced tooltip window based on Pretty_Text_Area. |
|
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} |
52483
478ef4fa3d5a
more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;
wenzelm
parents:
52481
diff
changeset
|
14 |
import javax.swing.{JWindow, JPanel, JComponent, PopupFactory} |
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 |
||
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
|
24 |
object Pretty_Tooltip |
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
|
25 |
{ |
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
|
26 |
/* 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
|
27 |
|
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 |
// owned by Swing thread |
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
|
29 |
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
|
30 |
|
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
|
31 |
private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] = |
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
|
32 |
{ |
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
|
33 |
Swing_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 |
|
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
|
39 |
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
|
40 |
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
|
41 |
parent: JComponent, |
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 |
rendering: Rendering, |
52483
478ef4fa3d5a
more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;
wenzelm
parents:
52481
diff
changeset
|
43 |
screen_point: Point, |
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
|
44 |
results: Command.Results, |
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
|
45 |
body: XML.Body): Pretty_Tooltip = |
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
|
46 |
{ |
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 |
Swing_Thread.require() |
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
|
48 |
|
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
|
49 |
val (old, rest) = |
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
|
50 |
JEdit_Lib.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) 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
|
51 |
case Some(tip) => hierarchy(tip).getOrElse((stack, Nil)) |
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
|
52 |
case None => (stack, Nil) |
51458
67542078fa21
prefer ownerless window, to avoid question of potentially changing parent view;
wenzelm
parents:
51457
diff
changeset
|
53 |
} |
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
|
54 |
old.foreach(_.hide_popup) |
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
|
55 |
|
52483
478ef4fa3d5a
more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;
wenzelm
parents:
52481
diff
changeset
|
56 |
val tip = new Pretty_Tooltip(view, rendering, parent, screen_point, results, body) |
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
|
57 |
stack = tip :: rest |
52484
23a09c639700
avoid potential race condition of focusLost/dismiss vs. popup.show;
wenzelm
parents:
52483
diff
changeset
|
58 |
tip.show_popup |
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
|
59 |
tip |
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
|
60 |
} |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
61 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
62 |
|
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
63 |
/* pending event and active state */ // owned by Swing thread |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
64 |
|
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
65 |
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
|
66 |
private var active = true |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
67 |
|
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
68 |
private val pending_delay = |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
69 |
Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) { |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
70 |
pending match { |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
71 |
case Some(body) => pending = None; body() |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
72 |
case None => |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
73 |
} |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
74 |
} |
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 |
def invoke(body: () => Unit): Unit = |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
77 |
Swing_Thread.required { |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
78 |
if (active) { |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
79 |
pending = Some(body) |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
80 |
pending_delay.invoke() |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
81 |
} |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
82 |
} |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
83 |
|
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
84 |
private lazy val reactivate_delay = |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
85 |
Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) { |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
86 |
active = true |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
87 |
} |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
88 |
|
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
89 |
private def deactivate(): Unit = |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
90 |
Swing_Thread.required { |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
91 |
pending = None |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
92 |
active = false |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
93 |
pending_delay.revoke() |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
94 |
reactivate_delay.invoke() |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
95 |
} |
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
|
96 |
|
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
97 |
|
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
98 |
/* dismiss */ |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
99 |
|
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
|
100 |
def dismiss(tip: Pretty_Tooltip) |
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
|
101 |
{ |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
102 |
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
|
103 |
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
|
104 |
case Some((old, _ :: rest)) => |
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
|
105 |
old.foreach(_.hide_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
|
106 |
tip.hide_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
|
107 |
stack = rest |
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
|
108 |
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
|
109 |
} |
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
|
110 |
} |
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
|
111 |
|
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 |
def dismiss_all() |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
113 |
{ |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52493
diff
changeset
|
114 |
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
|
115 |
stack.foreach(_.hide_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
|
116 |
stack = Nil |
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
|
117 |
} |
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
|
118 |
|
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
|
119 |
|
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
|
120 |
/* auxiliary geometry measurement */ |
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
|
121 |
|
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
|
122 |
private lazy val dummy_window = new JWindow |
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
|
123 |
|
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
|
124 |
private def decoration_size(tip: Pretty_Tooltip): (Int, Int) = |
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
|
125 |
{ |
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
|
126 |
val old_content = dummy_window.getContentPane |
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
|
127 |
|
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
|
128 |
dummy_window.setContentPane(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
|
129 |
dummy_window.pack |
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
|
130 |
dummy_window.revalidate |
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
|
131 |
|
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
|
132 |
val painter = tip.pretty_text_area.getPainter |
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 |
val w = dummy_window.getWidth - painter.getWidth |
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 |
val h = dummy_window.getHeight - painter.getHeight |
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
|
135 |
|
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
|
136 |
dummy_window.setContentPane(old_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
|
137 |
|
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
|
138 |
(w, h) |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
139 |
} |
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
|
140 |
} |
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
|
141 |
|
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
|
142 |
|
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
|
143 |
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
|
144 |
view: View, |
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 |
rendering: Rendering, |
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
|
146 |
parent: JComponent, |
52483
478ef4fa3d5a
more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;
wenzelm
parents:
52481
diff
changeset
|
147 |
screen_point: Point, |
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
|
148 |
results: Command.Results, |
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
|
149 |
body: XML.Body) extends JPanel(new BorderLayout) |
49702 | 150 |
{ |
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
|
151 |
tip => |
49705 | 152 |
|
49725 | 153 |
Swing_Thread.require() |
154 |
||
155 |
||
156 |
/* controls */ |
|
157 |
||
49727 | 158 |
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
|
159 |
icon = rendering.tooltip_close_icon |
49727 | 160 |
tooltip = "Close tooltip window" |
161 |
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
|
162 |
reactions += { case _: MouseClicked => Pretty_Tooltip.dismiss(tip) } |
49727 | 163 |
} |
164 |
||
49726 | 165 |
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
|
166 |
icon = rendering.tooltip_detach_icon |
49726 | 167 |
tooltip = "Detach tooltip window" |
168 |
listenTo(mouse.clicks) |
|
169 |
reactions += { |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50206
diff
changeset
|
170 |
case _: MouseClicked => |
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 |
Info_Dockable(view, rendering.snapshot, results, body) |
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
|
172 |
Pretty_Tooltip.dismiss(tip) |
49726 | 173 |
} |
174 |
} |
|
175 |
||
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
|
176 |
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
|
177 |
background = rendering.tooltip_color |
49709 | 178 |
} |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
179 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
180 |
|
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
|
181 |
/* 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
|
182 |
|
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
|
183 |
val 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
|
184 |
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
|
185 |
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
|
186 |
} |
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
|
187 |
|
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
|
188 |
pretty_text_area.addFocusListener(new FocusAdapter { |
52491
d435febab327
visually explicit focus (behaviour dependent on platform and look-and-feel);
wenzelm
parents:
52484
diff
changeset
|
189 |
override def focusGained(e: FocusEvent) |
d435febab327
visually explicit focus (behaviour dependent on platform and look-and-feel);
wenzelm
parents:
52484
diff
changeset
|
190 |
{ |
52493 | 191 |
tip_border(true) |
52491
d435febab327
visually explicit focus (behaviour dependent on platform and look-and-feel);
wenzelm
parents:
52484
diff
changeset
|
192 |
} |
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
|
193 |
override def focusLost(e: FocusEvent) |
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
|
194 |
{ |
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
|
195 |
Pretty_Tooltip.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
|
196 |
case Some((Nil, _)) => Pretty_Tooltip.dismiss(tip) |
52493 | 197 |
case _ => tip_border(false) |
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
|
198 |
} |
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
|
199 |
} |
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
|
200 |
}) |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
201 |
|
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
|
202 |
pretty_text_area.resize(Rendering.font_family(), |
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
|
203 |
Rendering.font_size("jedit_tooltip_font_scale").round) |
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 |
|
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 |
|
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 |
/* 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
|
207 |
|
52493 | 208 |
def tip_border(has_focus: Boolean) |
52491
d435febab327
visually explicit focus (behaviour dependent on platform and look-and-feel);
wenzelm
parents:
52484
diff
changeset
|
209 |
{ |
52493 | 210 |
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
|
211 |
tip.repaint() |
d435febab327
visually explicit focus (behaviour dependent on platform and look-and-feel);
wenzelm
parents:
52484
diff
changeset
|
212 |
} |
52493 | 213 |
tip_border(true) |
52491
d435febab327
visually explicit focus (behaviour dependent on platform and look-and-feel);
wenzelm
parents:
52484
diff
changeset
|
214 |
|
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
|
215 |
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
|
216 |
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
|
217 |
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
|
218 |
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
|
219 |
|
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 |
/* 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
|
222 |
|
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 |
private val popup = |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
224 |
{ |
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
|
225 |
val screen_bounds = JEdit_Lib.screen_bounds(screen_point) |
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
|
226 |
|
52492 | 227 |
val (w, h) = |
228 |
{ |
|
229 |
val painter = pretty_text_area.getPainter |
|
230 |
val metric = JEdit_Lib.pretty_metric(painter) |
|
231 |
val margin = rendering.tooltip_margin * metric.average |
|
232 |
||
233 |
val formatted = Pretty.formatted(body, margin, metric) |
|
234 |
val lines = |
|
235 |
XML.traverse_text(formatted)(0)( |
|
236 |
(n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) |
|
237 |
||
238 |
val (deco_width, deco_height) = Pretty_Tooltip.decoration_size(tip) |
|
239 |
val bounds = rendering.tooltip_bounds |
|
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
|
240 |
|
52492 | 241 |
val h1 = painter.getFontMetrics.getHeight * (lines + 1) + deco_height |
242 |
val h2 = (screen_bounds.height * bounds).toInt |
|
243 |
val h = h1 min h2 |
|
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
|
244 |
|
52492 | 245 |
val margin1 = |
246 |
if (h1 <= h2) |
|
247 |
(0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) }) |
|
248 |
else margin |
|
249 |
val w = |
|
250 |
((metric.unit * (margin1 + metric.average)).round.toInt + deco_width) min |
|
251 |
(screen_bounds.width * bounds).toInt |
|
252 |
||
253 |
(w, h) |
|
254 |
} |
|
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
|
255 |
|
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
|
256 |
tip.setSize(new Dimension(w, h)) |
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
|
257 |
tip.setPreferredSize(new Dimension(w, h)) |
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
|
258 |
|
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
|
259 |
val x = screen_point.x min (screen_bounds.x + screen_bounds.width - tip.getWidth) |
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
|
260 |
val y = screen_point.y min (screen_bounds.y + screen_bounds.height - tip.getHeight) |
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
|
261 |
PopupFactory.getSharedInstance.getPopup(parent, tip, x, y) |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
262 |
} |
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
|
263 |
|
52484
23a09c639700
avoid potential race condition of focusLost/dismiss vs. popup.show;
wenzelm
parents:
52483
diff
changeset
|
264 |
private def show_popup |
23a09c639700
avoid potential race condition of focusLost/dismiss vs. popup.show;
wenzelm
parents:
52483
diff
changeset
|
265 |
{ |
23a09c639700
avoid potential race condition of focusLost/dismiss vs. popup.show;
wenzelm
parents:
52483
diff
changeset
|
266 |
popup.show |
23a09c639700
avoid potential race condition of focusLost/dismiss vs. popup.show;
wenzelm
parents:
52483
diff
changeset
|
267 |
pretty_text_area.requestFocus |
23a09c639700
avoid potential race condition of focusLost/dismiss vs. popup.show;
wenzelm
parents:
52483
diff
changeset
|
268 |
pretty_text_area.update(rendering.snapshot, results, body) |
23a09c639700
avoid potential race condition of focusLost/dismiss vs. popup.show;
wenzelm
parents:
52483
diff
changeset
|
269 |
} |
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
|
270 |
|
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 |
private def hide_popup: Unit = popup.hide |
49702 | 272 |
} |
273 |