author | wenzelm |
Thu, 22 Nov 2012 17:11:26 +0100 | |
changeset 50169 | 071902349e3e |
parent 50168 | 4a575ef46466 |
child 50171 | d655dda100c5 |
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Thu Nov 22 17:01:20 2012 +0100 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Thu Nov 22 17:11:26 2012 +0100 @@ -115,6 +115,7 @@ val w = (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen.width / 2) val h = (font_metrics.getHeight * (lines + 2)) min (screen.height / 2) pretty_text_area.setPreferredSize(new Dimension(w, h)) + window.pack } { @@ -128,7 +129,6 @@ } window.setVisible(true) - window.pack pretty_text_area.refresh() }