--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sat Jun 29 21:28:24 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sat Jun 29 22:15:10 2013 +0200
@@ -55,6 +55,7 @@
val tip = new Pretty_Tooltip(view, rendering, parent, screen_point, results, body)
stack = tip :: rest
+ tip.show_popup
tip
}
@@ -221,9 +222,12 @@
PopupFactory.getSharedInstance.getPopup(parent, tip, x, y)
}
- popup.show
- pretty_text_area.requestFocus
- pretty_text_area.update(rendering.snapshot, results, body)
+ private def show_popup
+ {
+ popup.show
+ pretty_text_area.requestFocus
+ pretty_text_area.update(rendering.snapshot, results, body)
+ }
private def hide_popup: Unit = popup.hide
}