diff -r 788c8263e634 -r 6626bc5ed053 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 25 21:10:29 2012 +0100
@@ -47,8 +47,8 @@
   {
     Swing_Thread.require()
 
-    pretty_text_area.resize(PIDE.font_family(),
-      (PIDE.font_size("jedit_font_scale") * zoom_factor / 100).round)
+    pretty_text_area.resize(Rendering.font_family(),
+      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
   }
 
   private def handle_update(follow: Boolean, restriction: Option[Set[Command]])