--- 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"
--- 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
}
--- 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")
--- 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
}
--- 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]])
--- 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 =
- "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
- options.int("jedit_tooltip_font_size").toString + "px; \">" + // FIXME proper scaling (!?)
- HTML.encode(text) + "</pre></html>"
+ /* tooltip delay */
private val tooltip_lb = Time.seconds(0.5)
private val tooltip_ub = Time.seconds(60.0)
--- 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)
}