--- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Nov 21 13:47:47 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Wed Nov 21 14:06:59 2012 +0100
@@ -68,8 +68,8 @@
val pretty_text_area = new Pretty_Text_Area(view)
pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
- pretty_text_area.resize(
- Isabelle.font_family(), Isabelle.font_size("jedit_tooltip_font_scale").round)
+ pretty_text_area.resize(Isabelle.font_family(),
+ Isabelle.font_size("jedit_tooltip_font_scale").round)
pretty_text_area.update(rendering.snapshot, body)
pretty_text_area.registerKeyboardAction(action_listener, "close_all",