173 robust_body(()) { |
173 robust_body(()) { |
174 control = (e.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 |
174 control = (e.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 |
175 |
175 |
176 if ((control || hovering) && !buffer.isLoading) { |
176 if ((control || hovering) && !buffer.isLoading) { |
177 JEdit_Lib.buffer_lock(buffer) { |
177 JEdit_Lib.buffer_lock(buffer) { |
178 JEdit_Lib.pixel_range(text_area, e.getX(), e.getY()) match { |
178 JEdit_Lib.pixel_range(text_area, e.getX, e.getY) match { |
179 case None => active_reset() |
179 case None => active_reset() |
180 case Some(range) => |
180 case Some(range) => |
181 val rendering = get_rendering() |
181 val rendering = get_rendering() |
182 for ((area, require_control) <- active_areas) |
182 for ((area, require_control) <- active_areas) |
183 { |
183 { |
187 } |
187 } |
188 } |
188 } |
189 } |
189 } |
190 } |
190 } |
191 else active_reset() |
191 else active_reset() |
|
192 |
|
193 tooltip_event = Some(e) |
|
194 tooltip_delay.invoke() |
192 } |
195 } |
193 } |
196 } |
194 } |
197 } |
195 |
198 |
196 |
199 |
197 /* tooltips */ |
200 /* tooltips */ |
198 |
201 |
199 private val tooltip_painter = new TextAreaExtension |
202 private var tooltip_event: Option[MouseEvent] = None |
200 { |
203 |
201 override def getToolTipText(x: Int, y: Int): String = |
204 private val tooltip_delay = |
202 { |
205 Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) { |
203 robust_body(null: String) { |
206 tooltip_event match { |
204 val rendering = get_rendering() |
207 case Some(e) if e.getSource == text_area.getPainter => |
205 val snapshot = rendering.snapshot |
208 val rendering = get_rendering() |
206 if (!snapshot.is_outdated) { |
209 val snapshot = rendering.snapshot |
207 JEdit_Lib.pixel_range(text_area, x, y) match { |
210 if (!snapshot.is_outdated) { |
208 case None => |
211 val x = e.getX |
209 case Some(range) => |
212 val y = e.getY |
210 val tip = |
213 JEdit_Lib.pixel_range(text_area, x, y) match { |
211 if (control) rendering.tooltip(range) |
214 case None => |
212 else rendering.tooltip_message(range) |
215 case Some(range) => |
213 if (!tip.isEmpty) { |
216 val tip = |
214 val painter = text_area.getPainter |
217 if (control) rendering.tooltip(range) |
215 val y1 = y + painter.getFontMetrics.getHeight / 2 |
218 else rendering.tooltip_message(range) |
216 val results = rendering.command_results(range) |
219 if (!tip.isEmpty) { |
217 new Pretty_Tooltip(view, painter, rendering, x, y1, results, tip) |
220 val painter = text_area.getPainter |
218 } |
221 val y1 = y + painter.getFontMetrics.getHeight / 2 |
219 } |
222 val results = rendering.command_results(range) |
220 } |
223 new Pretty_Tooltip(view, painter, rendering, x, y1, results, tip) |
221 null |
224 } |
222 } |
225 } |
223 } |
226 } |
224 } |
227 tooltip_event = None |
|
228 case _ => |
|
229 } |
|
230 } |
225 |
231 |
226 |
232 |
227 /* text background */ |
233 /* text background */ |
228 |
234 |
229 private val background_painter = new TextAreaExtension |
235 private val background_painter = new TextAreaExtension |
505 |
511 |
506 def activate() |
512 def activate() |
507 { |
513 { |
508 val painter = text_area.getPainter |
514 val painter = text_area.getPainter |
509 painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state) |
515 painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state) |
510 painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter) |
|
511 painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) |
516 painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) |
512 painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) |
517 painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) |
513 painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1) |
518 painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1) |
514 painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1) |
519 painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1) |
515 painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2) |
520 painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2) |
539 painter.removeExtension(before_caret_painter2) |
544 painter.removeExtension(before_caret_painter2) |
540 painter.removeExtension(after_caret_painter1) |
545 painter.removeExtension(after_caret_painter1) |
541 painter.removeExtension(before_caret_painter1) |
546 painter.removeExtension(before_caret_painter1) |
542 painter.removeExtension(text_painter) |
547 painter.removeExtension(text_painter) |
543 painter.removeExtension(background_painter) |
548 painter.removeExtension(background_painter) |
544 painter.removeExtension(tooltip_painter) |
|
545 painter.removeExtension(set_state) |
549 painter.removeExtension(set_state) |
546 } |
550 } |
547 } |
551 } |
548 |
552 |