# HG changeset patch # User wenzelm # Date 1349428164 -7200 # Node ID 92ef8b638c6c760c75ba9ee60d994d384a2f809e # Parent 036c9a028dbd51f99201b1a54ff3cac7cb48bcbb tuned color and font size; diff -r 036c9a028dbd -r 92ef8b638c6c src/Tools/jEdit/etc/options --- 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" diff -r 036c9a028dbd -r 92ef8b638c6c src/Tools/jEdit/src/isabelle_rendering.scala --- 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") diff -r 036c9a028dbd -r 92ef8b638c6c src/Tools/jEdit/src/pretty_tooltip.scala --- 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() }