author | wenzelm |
Mon, 18 Mar 2013 19:33:25 +0100 | |
changeset 51457 | 66824fea1a72 |
parent 51452 | 14e6d761ba1c |
child 51458 | 67542078fa21 |
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 |
||
50554
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50538
diff
changeset
|
12 |
import java.awt.{Color, Point, BorderLayout, Window, Dimension} |
50743
44571ac53fed
propagate keys to enclosing view like org.gjt.sp.jedit.gui.CompletionPopup, but without its KeyEventInterceptor;
wenzelm
parents:
50726
diff
changeset
|
13 |
import java.awt.event.{WindowEvent, WindowAdapter, KeyEvent, KeyAdapter, KeyListener} |
50726
27478c11f63c
more elementary key handling: listen to low-level KEY_PRESSED events (without consuming);
wenzelm
parents:
50659
diff
changeset
|
14 |
import javax.swing.{SwingUtilities, JDialog, JPanel, JComponent} |
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 |
{ |
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 |
/* window stack -- owned by Swing thread */ |
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 |
|
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
|
28 |
private var window_stack: List[Pretty_Tooltip] = Nil |
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 |
|
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 |
def windows(): List[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
|
31 |
{ |
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 |
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
|
33 |
window_stack |
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
|
34 |
} |
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
|
35 |
|
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
|
36 |
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
|
37 |
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
|
38 |
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
|
39 |
rendering: Rendering, |
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 |
mouse_x: Int, mouse_y: Int, |
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 |
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
|
42 |
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
|
43 |
{ |
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 |
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
|
45 |
|
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 |
val parent_window = JEdit_Lib.parent_window(parent) getOrElse 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
|
47 |
|
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 |
val old_windows = |
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
|
49 |
windows().find(_ == parent_window) match { |
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
|
50 |
case None => windows() |
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 |
case Some(window) => window.descendants() |
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
|
52 |
} |
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
|
53 |
val window = |
51450
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
54 |
old_windows.reverse match { |
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
55 |
case Nil => |
51457 | 56 |
val window = new Pretty_Tooltip(view, parent_window) |
51450
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
57 |
window_stack = window :: window_stack |
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
58 |
window |
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
59 |
case window :: others => |
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
60 |
others.foreach(_.dispose) |
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
61 |
window |
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
|
62 |
} |
51457 | 63 |
window.init(rendering, parent, mouse_x, mouse_y, results, body) |
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
|
64 |
window |
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
|
65 |
} |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
66 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
67 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
68 |
/* global dismissed delay -- owned by Swing thread */ |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
69 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
70 |
private var active = true |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
71 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
72 |
private lazy val reactivate_delay = |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
73 |
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
|
74 |
active = true |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
75 |
} |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
76 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
77 |
def dismissed |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
78 |
{ |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
79 |
Swing_Thread.require() |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
80 |
active = false |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
81 |
reactivate_delay.invoke() |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
82 |
} |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
83 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
84 |
def is_active: Boolean = |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
85 |
{ |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
86 |
Swing_Thread.require() |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
87 |
active |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
88 |
} |
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
|
89 |
} |
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
|
90 |
|
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
|
91 |
|
51457 | 92 |
class Pretty_Tooltip private(view: View, parent_window: Window) |
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
|
93 |
extends JDialog(parent_window) |
49702 | 94 |
{ |
49705 | 95 |
window => |
96 |
||
49725 | 97 |
Swing_Thread.require() |
98 |
||
99 |
||
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
|
100 |
/* implicit state -- owned by Swing thread */ |
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
|
101 |
|
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
|
102 |
private var current_rendering: Rendering = |
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
|
103 |
Rendering(Document.State.init.snapshot(), PIDE.options.value) |
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
|
104 |
private var current_results = Command.Results.empty |
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
|
105 |
private var current_body: XML.Body = Nil |
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
|
106 |
|
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
|
107 |
|
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
|
108 |
/* window hierarchy */ |
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
|
109 |
|
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
|
110 |
def descendants(): List[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
|
111 |
if (Pretty_Tooltip.windows().exists(_ == window)) |
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
|
112 |
Pretty_Tooltip.windows().takeWhile(_ != window) |
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
|
113 |
else Nil |
50659
0f88591478e6
prefer JDialog over JWindow to avoid focus inversion problem on Compiz (e.g. Ubuntu/Unity 12.10): both JDialog and JFrame happen to work, but JFrame does not support parent nesting;
wenzelm
parents:
50554
diff
changeset
|
114 |
|
49705 | 115 |
window.addWindowFocusListener(new WindowAdapter { |
49712 | 116 |
override def windowLostFocus(e: WindowEvent) { |
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
|
117 |
if (!descendants().exists(_.isDisplayable)) |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
118 |
window.dismiss |
49712 | 119 |
} |
49702 | 120 |
}) |
49705 | 121 |
|
49702 | 122 |
|
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
|
123 |
/* main content */ |
49725 | 124 |
|
51450
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
125 |
window.setUndecorated(true) |
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
126 |
window.getRootPane.setBorder(new LineBorder(Color.BLACK)) |
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
127 |
|
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
|
128 |
private val content_panel = |
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
|
129 |
new JPanel(new BorderLayout) { override def getFocusTraversalKeysEnabled = false } |
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
|
130 |
window.setContentPane(content_panel) |
49725 | 131 |
|
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
132 |
val pretty_text_area = new Pretty_Text_Area(view, () => window.dismiss, true) { |
51451
e4203ebfe750
recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
wenzelm
parents:
51450
diff
changeset
|
133 |
override def get_background() = Some(current_rendering.tooltip_color) |
e4203ebfe750
recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
wenzelm
parents:
51450
diff
changeset
|
134 |
} |
49706 | 135 |
window.add(pretty_text_area) |
49708 | 136 |
|
49725 | 137 |
|
138 |
/* controls */ |
|
139 |
||
49727 | 140 |
private val close = new Label { |
50199
6d04e2422769
quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents:
50169
diff
changeset
|
141 |
icon = Rendering.tooltip_close_icon |
49727 | 142 |
tooltip = "Close tooltip window" |
143 |
listenTo(mouse.clicks) |
|
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
144 |
reactions += { case _: MouseClicked => window.dismiss } |
49727 | 145 |
} |
146 |
||
49726 | 147 |
private val detach = new Label { |
50199
6d04e2422769
quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents:
50169
diff
changeset
|
148 |
icon = Rendering.tooltip_detach_icon |
49726 | 149 |
tooltip = "Detach tooltip window" |
150 |
listenTo(mouse.clicks) |
|
151 |
reactions += { |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50206
diff
changeset
|
152 |
case _: MouseClicked => |
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
|
153 |
Info_Dockable(view, current_rendering.snapshot, current_results, current_body) |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
154 |
window.dismiss |
49726 | 155 |
} |
156 |
} |
|
157 |
||
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
|
158 |
private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) |
49725 | 159 |
window.add(controls.peer, BorderLayout.NORTH) |
160 |
||
161 |
||
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
162 |
/* init */ |
49725 | 163 |
|
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
|
164 |
def init( |
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
|
165 |
rendering: Rendering, |
51457 | 166 |
parent: JComponent, |
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
|
167 |
mouse_x: Int, mouse_y: Int, |
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
|
168 |
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
|
169 |
body: XML.Body) |
49708 | 170 |
{ |
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
|
171 |
current_rendering = rendering |
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
|
172 |
current_results = 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
|
173 |
current_body = body |
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
|
174 |
|
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
|
175 |
pretty_text_area.resize(Rendering.font_family(), |
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
|
176 |
Rendering.font_size("jedit_tooltip_font_scale").round) |
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
|
177 |
pretty_text_area.update(rendering.snapshot, results, body) |
49707 | 178 |
|
51451
e4203ebfe750
recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
wenzelm
parents:
51450
diff
changeset
|
179 |
content_panel.setBackground(rendering.tooltip_color) |
e4203ebfe750
recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
wenzelm
parents:
51450
diff
changeset
|
180 |
controls.background = rendering.tooltip_color |
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
|
181 |
|
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
|
182 |
|
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
|
183 |
/* window geometry */ |
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
|
184 |
|
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
|
185 |
val screen_point = new Point(mouse_x, mouse_y) |
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
|
186 |
SwingUtilities.convertPointToScreen(screen_point, parent) |
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
|
187 |
val screen_bounds = JEdit_Lib.screen_bounds(screen_point) |
51439
b10b64679c5b
more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible);
wenzelm
parents:
50915
diff
changeset
|
188 |
|
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
|
189 |
{ |
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
|
190 |
val painter = pretty_text_area.getPainter |
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
|
191 |
val fm = painter.getFontMetrics |
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
|
192 |
val margin = rendering.tooltip_margin |
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
|
193 |
val lines = |
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
|
194 |
XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)( |
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
|
195 |
(n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) |
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
|
196 |
|
51450
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
197 |
if (window.getWidth == 0) { |
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
198 |
window.setSize(new Dimension(100, 100)) |
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
199 |
window.setPreferredSize(new Dimension(100, 100)) |
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
200 |
} |
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
|
201 |
window.pack |
51450
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
202 |
window.revalidate |
a8e3a72b348c
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm
parents:
51449
diff
changeset
|
203 |
|
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
|
204 |
val deco_width = window.getWidth - painter.getWidth |
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
|
205 |
val deco_height = window.getHeight - painter.getHeight |
51439
b10b64679c5b
more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible);
wenzelm
parents:
50915
diff
changeset
|
206 |
|
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
|
207 |
val bounds = rendering.tooltip_bounds |
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
|
208 |
val w = |
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
|
209 |
((Pretty.char_width(fm) * (margin + 1)).round.toInt + deco_width) min |
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
|
210 |
(screen_bounds.width * bounds).toInt |
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
|
211 |
val h = |
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
|
212 |
(fm.getHeight * (lines + 1) + deco_height) min |
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
|
213 |
(screen_bounds.height * bounds).toInt |
49706 | 214 |
|
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
|
215 |
window.setSize(new Dimension(w, h)) |
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
|
216 |
window.setPreferredSize(new Dimension(w, h)) |
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
|
217 |
window.pack |
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
|
218 |
window.revalidate |
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
|
219 |
|
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
|
220 |
val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth) |
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
|
221 |
val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight) |
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
|
222 |
window.setLocation(x, y) |
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
|
223 |
} |
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
|
224 |
|
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
|
225 |
window.setVisible(true) |
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
|
226 |
pretty_text_area.requestFocus |
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
|
227 |
pretty_text_area.refresh() |
49709 | 228 |
} |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
229 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
230 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
231 |
/* dismiss */ |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
232 |
|
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
233 |
def dismiss |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
234 |
{ |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
235 |
Swing_Thread.require() |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
236 |
Pretty_Tooltip.dismissed |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
237 |
window.dispose |
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51451
diff
changeset
|
238 |
} |
49702 | 239 |
} |
240 |