# HG changeset patch
# User wenzelm
# Date 1372530333 -7200
# Node ID d977e7eb7839169edbba37e9ea561ea7d1896b7c
# Parent  6a762cda56bddfddad40b0e2a1e959d39823b071
update text only once;

diff -r 6a762cda56bd -r d977e7eb7839 src/Tools/jEdit/src/pretty_tooltip.scala
--- 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
 }