# HG changeset patch
# User wenzelm
# Date 1349375770 -7200
# Node ID c89fffb11769356932b41c63c65c2fcc04d0be81
# Parent  696e91c0bc801411d7a6dd5c0bc74d3825a8dda9
some re-ordering of initialization to ensure proper formatting;

diff -r 696e91c0bc80 -r c89fffb11769 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Oct 04 20:14:40 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Oct 04 20:36:10 2012 +0200
@@ -34,11 +34,6 @@
     point
   }
 
-  val pretty_text_area = new Pretty_Text_Area(view)
-  pretty_text_area.resize(
-    Isabelle.font_family(), Isabelle.font_size("jedit_tooltip_font_scale").round)
-  pretty_text_area.update(rendering.snapshot, body)
-
   addWindowFocusListener(new WindowAdapter {
     override def windowLostFocus(e: WindowEvent) { dispose() }
   })
@@ -47,9 +42,17 @@
   })
   getRootPane.setBorder(new LineBorder(Color.BLACK))
 
-  add(pretty_text_area)
+  setLocation(point.x, point.y)
   setSize(fm.charWidth(Pretty.spc) * Isabelle.options.int("jedit_tooltip_margin"), 100)
-  setLocation(point.x, point.y)
+
+  val pretty_text_area = new Pretty_Text_Area(view)
+  add(pretty_text_area)
+
+  pretty_text_area.resize(
+    Isabelle.font_family(), Isabelle.font_size("jedit_tooltip_font_scale").round)
+  pretty_text_area.update(rendering.snapshot, body)
+
   setVisible(true)
+  pretty_text_area.refresh()
 }