update text only once;

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jun 29 18:20:09 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jun 29 20:25:33 2013 +0200
@@ -179,7 +179,6 @@
 
   pretty_text_area.resize(Rendering.font_family(),
     Rendering.font_size("jedit_tooltip_font_scale").round)
-  pretty_text_area.update(rendering.snapshot, results, body)
 
 
   /* main content */
@@ -226,7 +225,7 @@
 
   popup.show
   pretty_text_area.requestFocus
-  pretty_text_area.refresh()
+  pretty_text_area.update(rendering.snapshot, results, body)
 
   private def hide_popup: Unit = popup.hide
 }