# HG changeset patch # User wenzelm # Date 1349371910 -7200 # Node ID e2762f962042c6323acee1be5ca7d170fdc6398f # Parent 2d1cbdf6a68bd0007d0f6447df1d8cbb844b0d75 refined rich tooltip options; basic tooltips without markup; diff -r 2d1cbdf6a68b -r e2762f962042 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Thu Oct 04 18:28:31 2012 +0200 +++ b/src/Tools/jEdit/etc/options Thu Oct 04 19:31:50 2012 +0200 @@ -9,8 +9,8 @@ option jedit_font_scale : real = 1.0 -- "scale factor of add-on panels wrt. main text area" -option jedit_tooltip_font_size : int = 10 - -- "tooltip font size (according to HTML)" +option jedit_tooltip_font_scale : real = 0.85 + -- "scale factor of tooltips wrt. main text area" option jedit_tooltip_margin : int = 60 -- "margin for tooltip pretty-printing" diff -r 2d1cbdf6a68b -r e2762f962042 src/Tools/jEdit/src/isabelle_logic.scala --- a/src/Tools/jEdit/src/isabelle_logic.scala Thu Oct 04 18:28:31 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Thu Oct 04 19:31:50 2012 +0200 @@ -56,7 +56,7 @@ component.listenTo(component.selection) component.reactions += { case SelectionChanged(_) => component.save() } } - component.tooltip = Isabelle.tooltip(Isabelle.options.value.check_name(opt_name).print_default) + component.tooltip = Isabelle.options.value.check_name(opt_name).print_default component } diff -r 2d1cbdf6a68b -r e2762f962042 src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Thu Oct 04 18:28:31 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_options.scala Thu Oct 04 19:31:50 2012 +0200 @@ -42,7 +42,7 @@ // FIXME avoid hard-wired stuff private val relevant_options = Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview", - "jedit_tooltip_font_size", "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", + "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_update_delay", "editor_reparse_limit") diff -r 2d1cbdf6a68b -r e2762f962042 src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala Thu Oct 04 18:28:31 2012 +0200 +++ b/src/Tools/jEdit/src/jedit_options.scala Thu Oct 04 19:31:50 2012 +0200 @@ -44,7 +44,7 @@ def load = button.setSelectedColor(Color_Value(string(opt_name))) def save = string(opt_name) = Color_Value.print(button.getSelectedColor) } - component.tooltip = Isabelle.tooltip(opt.print_default) + component.tooltip = opt.print_default component } @@ -91,7 +91,7 @@ text_area } component.load() - component.tooltip = Isabelle.tooltip(opt.print_default) + component.tooltip = opt.print_default component } diff -r 2d1cbdf6a68b -r e2762f962042 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Thu Oct 04 18:28:31 2012 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Thu Oct 04 19:31:50 2012 +0200 @@ -48,7 +48,7 @@ Swing_Thread.require() pretty_text_area.resize(Isabelle.font_family(), - scala.math.round(Isabelle.font_size() * zoom_factor / 100)) + scala.math.round(Isabelle.font_size("jedit_font_scale") * zoom_factor / 100)) } private def handle_update(follow: Boolean, restriction: Option[Set[Command]]) diff -r 2d1cbdf6a68b -r e2762f962042 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Thu Oct 04 18:28:31 2012 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Thu Oct 04 19:31:50 2012 +0200 @@ -51,16 +51,11 @@ def font_family(): String = jEdit.getProperty("view.font") - def font_size(): Float = - (jEdit.getIntegerProperty("view.fontsize", 16) * options.real("jedit_font_scale")).toFloat + def font_size(scale: String): Float = + (jEdit.getIntegerProperty("view.fontsize", 16) * options.real(scale)).toFloat - /* tooltip markup */ - - def tooltip(text: String): String = - "
" +  // FIXME proper scaling (!?)
-      HTML.encode(text) + "
" + /* tooltip delay */ private val tooltip_lb = Time.seconds(0.5) private val tooltip_ub = Time.seconds(60.0) diff -r 2d1cbdf6a68b -r e2762f962042 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Thu Oct 04 18:28:31 2012 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Oct 04 19:31:50 2012 +0200 @@ -202,6 +202,9 @@ val rendering = get_rendering() val snapshot = rendering.snapshot if (!snapshot.is_outdated) { + val painter = text_area.getPainter + val fm = painter.getFontMetrics + val offset = text_area.xyToOffset(x, y) val range = Text.Range(offset, offset + 1) val tip = @@ -209,15 +212,16 @@ else rendering.tooltip_message(range) if (!tip.isEmpty) { val point = { - val painter = text_area.getPainter val bounds = painter.getBounds() - val point = new Point(bounds.x + x, bounds.y + painter.getFontMetrics.getHeight + y) + val point = new Point(bounds.x + x, bounds.y + fm.getHeight + y) SwingUtilities.convertPointToScreen(point, painter) point } val tooltip_text = new Pretty_Text_Area(view) - tooltip_text.resize(Isabelle.font_family(), Isabelle.font_size().round) // FIXME tooltip_scale + tooltip_text.resize(Isabelle.font_family(), + Isabelle.font_size("jedit_tooltip_font_scale").round) + tooltip_text.update(snapshot, tip) val window = new JWindow(view) { @@ -230,7 +234,7 @@ getRootPane.setBorder(new LineBorder(Color.BLACK)) add(tooltip_text) - setSize(300, 100) + setSize(fm.charWidth(Pretty.spc) * Isabelle.options.int("jedit_tooltip_margin"), 100) setLocation(point.x, point.y) setVisible(true) }