tuned color and font size;

--- a/src/Tools/jEdit/etc/options	Fri Oct 05 10:54:07 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Fri Oct 05 11:09:24 2012 +0200
@@ -30,6 +30,7 @@
 option running_color : string = "610061FF"
 option running1_color : string = "61006164"
 option light_color : string = "F0F0F0FF"
+option tooltip_color : string = "FFFFE9FF"
 option writeln_color : string = "C0C0C0FF"
 option warning_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Oct 05 10:54:07 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Oct 05 11:09:24 2012 +0200
@@ -112,6 +112,7 @@
   val running_color = color_value("running_color")
   val running1_color = color_value("running1_color")
   val light_color = color_value("light_color")
+  val tooltip_color = color_value("tooltip_color")
   val writeln_color = color_value("writeln_color")
   val warning_color = color_value("warning_color")
   val error_color = color_value("error_color")

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 10:54:07 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 11:09:24 2012 +0200
@@ -26,10 +26,9 @@
 {
   window =>
 
-  private val painter = text_area.getPainter
-  private val fm = painter.getFontMetrics
-
   private val point = {
+    val painter = text_area.getPainter
+    val fm = painter.getFontMetrics
     val bounds = painter.getBounds()
     val point = new Point(bounds.x + x, bounds.y + fm.getHeight + y)
     SwingUtilities.convertPointToScreen(point, painter)
@@ -56,16 +55,17 @@
   })
   window.getRootPane.setBorder(new LineBorder(Color.BLACK))
 
-  window.setLocation(point.x, point.y)
-  window.setSize(fm.charWidth(Pretty.spc) * Isabelle.options.int("jedit_tooltip_margin"), 100)
-
   val pretty_text_area = new Pretty_Text_Area(view)
-  window.add(pretty_text_area)
-
+  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.update(rendering.snapshot, body)
 
+  window.add(pretty_text_area)
+  window.setLocation(point.x, point.y)
+  window.setSize(pretty_text_area.getPainter.getFontMetrics.charWidth(Pretty.spc) *
+    Isabelle.options.int("jedit_tooltip_margin"), 100)
+
   window.setVisible(true)
   pretty_text_area.refresh()
 }