src/Tools/jEdit/src/pretty_tooltip.scala

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -199,8 +199,7 @@
     }
   })
 
-  pretty_text_area.resize(Rendering.font_family(),
-    Rendering.font_size("jedit_popup_font_scale").round)
+  pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_popup_font_scale")))
 
 
   /* main content */