equal
deleted
inserted
replaced
49 windows().find(_ == parent_window) match { |
49 windows().find(_ == parent_window) match { |
50 case None => windows() |
50 case None => windows() |
51 case Some(window) => window.descendants() |
51 case Some(window) => window.descendants() |
52 } |
52 } |
53 val window = |
53 val window = |
54 if (old_windows.isEmpty) { |
54 old_windows.reverse match { |
55 val window = new Pretty_Tooltip(view, parent, parent_window) |
55 case Nil => |
56 window_stack = window :: window_stack |
56 val window = new Pretty_Tooltip(view, parent, parent_window) |
57 window |
57 window_stack = window :: window_stack |
58 } |
58 window |
59 else { |
59 case window :: others => |
60 old_windows.foreach(_.dispose) |
60 others.foreach(_.dispose) |
61 old_windows.last |
61 window |
62 } |
62 } |
63 window.init(rendering, mouse_x, mouse_y, results, body) |
63 window.init(rendering, mouse_x, mouse_y, results, body) |
64 window |
64 window |
65 } |
65 } |
66 } |
66 } |
96 } |
96 } |
97 }) |
97 }) |
98 |
98 |
99 |
99 |
100 /* main content */ |
100 /* main content */ |
|
101 |
|
102 window.setUndecorated(true) |
|
103 window.getRootPane.setBorder(new LineBorder(Color.BLACK)) |
101 |
104 |
102 private val content_panel = |
105 private val content_panel = |
103 new JPanel(new BorderLayout) { override def getFocusTraversalKeysEnabled = false } |
106 new JPanel(new BorderLayout) { override def getFocusTraversalKeysEnabled = false } |
104 window.setContentPane(content_panel) |
107 window.setContentPane(content_panel) |
105 |
108 |
141 { |
144 { |
142 current_rendering = rendering |
145 current_rendering = rendering |
143 current_results = results |
146 current_results = results |
144 current_body = body |
147 current_body = body |
145 |
148 |
146 window.setUndecorated(true) |
|
147 window.setFocusableWindowState(true) |
|
148 window.getRootPane.setBorder(new LineBorder(Color.BLACK)) |
|
149 |
|
150 pretty_text_area.resize(Rendering.font_family(), |
149 pretty_text_area.resize(Rendering.font_family(), |
151 Rendering.font_size("jedit_tooltip_font_scale").round) |
150 Rendering.font_size("jedit_tooltip_font_scale").round) |
152 pretty_text_area.update(rendering.snapshot, results, body) |
151 pretty_text_area.update(rendering.snapshot, results, body) |
153 |
152 |
154 val background = rendering.tooltip_color |
153 val background = rendering.tooltip_color |
170 val margin = rendering.tooltip_margin |
169 val margin = rendering.tooltip_margin |
171 val lines = |
170 val lines = |
172 XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)( |
171 XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)( |
173 (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) |
172 (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) |
174 |
173 |
175 window.setSize(new Dimension(100, 100)) |
174 if (window.getWidth == 0) { |
176 window.setPreferredSize(new Dimension(100, 100)) |
175 window.setSize(new Dimension(100, 100)) |
|
176 window.setPreferredSize(new Dimension(100, 100)) |
|
177 } |
177 window.pack |
178 window.pack |
|
179 window.revalidate |
|
180 |
178 val deco_width = window.getWidth - painter.getWidth |
181 val deco_width = window.getWidth - painter.getWidth |
179 val deco_height = window.getHeight - painter.getHeight |
182 val deco_height = window.getHeight - painter.getHeight |
180 |
183 |
181 val bounds = rendering.tooltip_bounds |
184 val bounds = rendering.tooltip_bounds |
182 val w = |
185 val w = |