--- a/src/Tools/jEdit/etc/options Sat Mar 16 20:51:47 2013 +0100
+++ b/src/Tools/jEdit/etc/options Sat Mar 16 21:44:04 2013 +0100
@@ -6,6 +6,9 @@
option jedit_font_scale : real = 1.0
-- "scale factor of add-on panels wrt. main text area"
+option jedit_tooltip_delay : real = 0.75
+ -- "delay for semantic tooltip popup"
+
option jedit_tooltip_font_scale : real = 0.85
-- "scale factor of tooltips wrt. main text area"
--- a/src/Tools/jEdit/src/isabelle_options.scala Sat Mar 16 20:51:47 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala Sat Mar 16 21:44:04 2013 +0100
@@ -42,11 +42,11 @@
// FIXME avoid hard-wired stuff
private val relevant_options =
Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
- "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_font_scale",
- "jedit_tooltip_margin", "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
- "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay",
- "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
- "editor_update_delay", "editor_chart_delay")
+ "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_delay",
+ "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter", "threads",
+ "threads_trace", "parallel_proofs", "parallel_subproofs_saturation", "editor_load_delay",
+ "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
+ "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
relevant_options.foreach(PIDE.options.value.check_name _)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 16 20:51:47 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 16 21:44:04 2013 +0100
@@ -93,23 +93,22 @@
}
getPainter.setFoldLineStyle(fold_line_style)
+ getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
+ getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
+ background.map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
+ getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
+ getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
+ getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
+ getGutter.setBorder(0,
+ jEdit.getColorProperty("view.gutter.focusBorderColor"),
+ jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
+ getPainter.getBackground)
+ getGutter.setFoldPainter(getFoldPainter)
+ getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
+
if (getWidth > 0) {
- getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
- getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
- background.map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
- getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
- getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
- getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
- getGutter.setBorder(0,
- jEdit.getColorProperty("view.gutter.focusBorderColor"),
- jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
- getPainter.getBackground)
- getGutter.setFoldPainter(getFoldPainter)
-
- getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
-
val fm = getPainter.getFontMetrics
- val margin = ((getWidth - getGutter.getWidth) / (Pretty.char_width_int(fm) max 1) - 2) max 20
+ val margin = (getPainter.getWidth / (Pretty.char_width_int(fm) max 1)) max 20
val base_snapshot = current_base_snapshot
val base_results = current_base_results
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 16 20:51:47 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 16 21:44:04 2013 +0100
@@ -97,17 +97,31 @@
val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
{
- val fm = pretty_text_area.getPainter.getFontMetrics
+ val painter = pretty_text_area.getPainter
+ val fm = painter.getFontMetrics
val margin = rendering.tooltip_margin
val lines =
XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)(
(n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
+ window.setSize(new Dimension(100, 100))
+ window.setPreferredSize(new Dimension(100, 100))
+ window.pack
+ val deco_width = window.getWidth - painter.getWidth
+ val deco_height = window.getHeight - painter.getHeight
+
val bounds = rendering.tooltip_bounds
- val w = (Pretty.char_width_int(fm) * (margin + 2)) min (screen_bounds.width * bounds).toInt
- val h = (fm.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt
- pretty_text_area.setPreferredSize(new Dimension(w, h))
+ val w =
+ ((Pretty.char_width(fm) * (margin + 1)).round.toInt + deco_width) min
+ (screen_bounds.width * bounds).toInt
+ val h =
+ (fm.getHeight * (lines + 1) + deco_height) min
+ (screen_bounds.height * bounds).toInt
+
+ window.setSize(new Dimension(w, h))
+ window.setPreferredSize(new Dimension(w, h))
window.pack
+ window.revalidate
val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
--- a/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 16 20:51:47 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 16 21:44:04 2013 +0100
@@ -175,7 +175,7 @@
if ((control || hovering) && !buffer.isLoading) {
JEdit_Lib.buffer_lock(buffer) {
- JEdit_Lib.pixel_range(text_area, e.getX(), e.getY()) match {
+ JEdit_Lib.pixel_range(text_area, e.getX, e.getY) match {
case None => active_reset()
case Some(range) =>
val rendering = get_rendering()
@@ -189,6 +189,9 @@
}
}
else active_reset()
+
+ tooltip_event = Some(e)
+ tooltip_delay.invoke()
}
}
}
@@ -196,32 +199,35 @@
/* tooltips */
- private val tooltip_painter = new TextAreaExtension
- {
- override def getToolTipText(x: Int, y: Int): String =
- {
- robust_body(null: String) {
- val rendering = get_rendering()
- val snapshot = rendering.snapshot
- if (!snapshot.is_outdated) {
- JEdit_Lib.pixel_range(text_area, x, y) match {
- case None =>
- case Some(range) =>
- val tip =
- if (control) rendering.tooltip(range)
- else rendering.tooltip_message(range)
- if (!tip.isEmpty) {
- val painter = text_area.getPainter
- val y1 = y + painter.getFontMetrics.getHeight / 2
- val results = rendering.command_results(range)
- new Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
- }
+ private var tooltip_event: Option[MouseEvent] = None
+
+ private val tooltip_delay =
+ Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
+ tooltip_event match {
+ case Some(e) if e.getSource == text_area.getPainter =>
+ val rendering = get_rendering()
+ val snapshot = rendering.snapshot
+ if (!snapshot.is_outdated) {
+ val x = e.getX
+ val y = e.getY
+ JEdit_Lib.pixel_range(text_area, x, y) match {
+ case None =>
+ case Some(range) =>
+ val tip =
+ if (control) rendering.tooltip(range)
+ else rendering.tooltip_message(range)
+ if (!tip.isEmpty) {
+ val painter = text_area.getPainter
+ val y1 = y + painter.getFontMetrics.getHeight / 2
+ val results = rendering.command_results(range)
+ new Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
+ }
+ }
}
- }
- null
+ tooltip_event = None
+ case _ =>
}
}
- }
/* text background */
@@ -507,7 +513,6 @@
{
val painter = text_area.getPainter
painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
- painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
@@ -541,7 +546,6 @@
painter.removeExtension(before_caret_painter1)
painter.removeExtension(text_painter)
painter.removeExtension(background_painter)
- painter.removeExtension(tooltip_painter)
painter.removeExtension(set_state)
}
}