# HG changeset patch # User wenzelm # Date 1363466644 -3600 # Node ID 8d3614b82c80e4bf8d691ece009bc7b86eef2b44 # Parent a614e456870b515bf897907bb4c3e3324c2158b0# Parent 37f699750430e2b58d4562120de3be92ae18b9bc merged diff -r a614e456870b -r 8d3614b82c80 src/Tools/jEdit/etc/options --- 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" diff -r a614e456870b -r 8d3614b82c80 src/Tools/jEdit/src/isabelle_options.scala --- 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 _) diff -r a614e456870b -r 8d3614b82c80 src/Tools/jEdit/src/pretty_text_area.scala --- 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 diff -r a614e456870b -r 8d3614b82c80 src/Tools/jEdit/src/pretty_tooltip.scala --- 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) diff -r a614e456870b -r 8d3614b82c80 src/Tools/jEdit/src/rich_text_area.scala --- 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) } }