equal
deleted
inserted
replaced
121 def tooltip(text: String): String = |
121 def tooltip(text: String): String = |
122 "<html><pre style=\"font-family: " + font_family() + "; font-size: " + |
122 "<html><pre style=\"font-family: " + font_family() + "; font-size: " + |
123 Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?) |
123 Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?) |
124 HTML.encode(text) + "</pre></html>" |
124 HTML.encode(text) + "</pre></html>" |
125 |
125 |
|
126 private val tooltip_lb = Time.seconds(0.5) |
|
127 private val tooltip_ub = Time.seconds(60.0) |
126 def tooltip_dismiss_delay(): Time = |
128 def tooltip_dismiss_delay(): Time = |
127 Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5) |
129 Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub |
128 |
130 |
129 def setup_tooltips() |
131 def setup_tooltips() |
130 { |
132 { |
131 Swing_Thread.now { |
133 Swing_Thread.now { |
132 val manager = javax.swing.ToolTipManager.sharedInstance |
134 val manager = javax.swing.ToolTipManager.sharedInstance |