# HG changeset patch # User wenzelm # Date 1363609122 -3600 # Node ID d2bc229e1f37cf60b6ac8dfe505fbebbd0ecc287 # Parent b041137f7fe54fea16b20855f379a016be500011# Parent 14e6d761ba1c1caf8f11bce3cfb31758ea8b89c4 merged diff -r b041137f7fe5 -r d2bc229e1f37 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Mon Mar 18 12:31:13 2013 +0100 +++ b/src/Tools/jEdit/etc/options Mon Mar 18 13:18:42 2013 +0100 @@ -7,7 +7,7 @@ -- "scale factor of add-on panels wrt. main text area" option jedit_tooltip_delay : real = 0.75 - -- "delay for semantic tooltip popup" + -- "open/close delay for document tooltips" option jedit_tooltip_font_scale : real = 0.85 -- "scale factor of tooltips wrt. main text area" diff -r b041137f7fe5 -r d2bc229e1f37 src/Tools/jEdit/src/graphview_dockable.scala --- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Mar 18 12:31:13 2013 +0100 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Mar 18 13:18:42 2013 +0100 @@ -65,7 +65,7 @@ override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = { val rendering = Rendering(snapshot, PIDE.options.value) - new Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body) + Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body) null } } diff -r b041137f7fe5 -r d2bc229e1f37 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Mar 18 12:31:13 2013 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon Mar 18 13:18:42 2013 +0100 @@ -54,7 +54,6 @@ class Pretty_Text_Area( view: View, - background: Option[Color] = None, close_action: () => Unit = () => (), propagate_keys: Boolean = false) extends JEditEmbeddedTextArea { @@ -75,6 +74,8 @@ new Rich_Text_Area(view, text_area, () => current_rendering, close_action, caret_visible = false, hovering = true) + def get_background(): Option[Color] = None + def refresh() { Swing_Thread.require() @@ -95,7 +96,7 @@ getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor")) getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor")) - background.map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) }) + get_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")) @@ -169,10 +170,7 @@ Registers.copy(text_area, '$') evt.consume case KeyEvent.VK_ESCAPE => - Window.getWindows foreach { - case c: Pretty_Tooltip => c.dispose - case _ => - } + Pretty_Tooltip.windows().foreach(_.dismiss) evt.consume case _ => } diff -r b041137f7fe5 -r d2bc229e1f37 src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Mar 18 12:31:13 2013 +0100 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Mon Mar 18 13:18:42 2013 +0100 @@ -21,46 +21,117 @@ import org.gjt.sp.jedit.textarea.TextArea -class Pretty_Tooltip( - view: View, - parent: JComponent, - rendering: Rendering, - mouse_x: Int, mouse_y: Int, - results: Command.Results, - body: XML.Body) - extends JDialog(JEdit_Lib.parent_window(parent) getOrElse view) +object Pretty_Tooltip +{ + /* window stack -- owned by Swing thread */ + + private var window_stack: List[Pretty_Tooltip] = Nil + + def windows(): List[Pretty_Tooltip] = + { + Swing_Thread.require() + window_stack + } + + def apply( + view: View, + parent: JComponent, + rendering: Rendering, + mouse_x: Int, mouse_y: Int, + results: Command.Results, + body: XML.Body): Pretty_Tooltip = + { + Swing_Thread.require() + + val parent_window = JEdit_Lib.parent_window(parent) getOrElse view + + val old_windows = + windows().find(_ == parent_window) match { + case None => windows() + case Some(window) => window.descendants() + } + val window = + old_windows.reverse match { + case Nil => + val window = new Pretty_Tooltip(view, parent, parent_window) + window_stack = window :: window_stack + window + case window :: others => + others.foreach(_.dispose) + window + } + window.init(rendering, mouse_x, mouse_y, results, body) + window + } + + + /* global dismissed delay -- owned by Swing thread */ + + private var active = true + + private lazy val reactivate_delay = + Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) { + active = true + } + + def dismissed + { + Swing_Thread.require() + active = false + reactivate_delay.invoke() + } + + def is_active: Boolean = + { + Swing_Thread.require() + active + } +} + + +class Pretty_Tooltip private(view: View, parent: JComponent, parent_window: Window) + extends JDialog(parent_window) { window => Swing_Thread.require() - window.setUndecorated(true) - window.setFocusableWindowState(true) + /* implicit state -- owned by Swing thread */ + + private var current_rendering: Rendering = + Rendering(Document.State.init.snapshot(), PIDE.options.value) + private var current_results = Command.Results.empty + private var current_body: XML.Body = Nil + + + /* window hierarchy */ + + def descendants(): List[Pretty_Tooltip] = + if (Pretty_Tooltip.windows().exists(_ == window)) + Pretty_Tooltip.windows().takeWhile(_ != window) + else Nil window.addWindowFocusListener(new WindowAdapter { override def windowLostFocus(e: WindowEvent) { - if (!Window.getWindows.exists(w => - w.isDisplayable && JEdit_Lib.ancestors(w).exists(_ == window))) - window.dispose() + if (!descendants().exists(_.isDisplayable)) + window.dismiss } }) - window.setContentPane(new JPanel(new BorderLayout) { - setBackground(rendering.tooltip_color) - override def getFocusTraversalKeysEnabled(): Boolean = false - }) + + /* main content */ + + window.setUndecorated(true) window.getRootPane.setBorder(new LineBorder(Color.BLACK)) - - /* pretty text area */ + private val content_panel = + new JPanel(new BorderLayout) { override def getFocusTraversalKeysEnabled = false } + window.setContentPane(content_panel) - val pretty_text_area = - new Pretty_Text_Area(view, Some(rendering.tooltip_color), () => window.dispose(), true) - pretty_text_area.resize(Rendering.font_family(), - Rendering.font_size("jedit_tooltip_font_scale").round) - pretty_text_area.update(rendering.snapshot, results, body) - + val pretty_text_area = new Pretty_Text_Area(view, () => window.dismiss, true) { + override def get_background() = Some(current_rendering.tooltip_color) + } window.add(pretty_text_area) @@ -70,7 +141,7 @@ icon = Rendering.tooltip_close_icon tooltip = "Close tooltip window" listenTo(mouse.clicks) - reactions += { case _: MouseClicked => window.dispose() } + reactions += { case _: MouseClicked => window.dismiss } } private val detach = new Label { @@ -79,57 +150,90 @@ listenTo(mouse.clicks) reactions += { case _: MouseClicked => - Info_Dockable(view, rendering.snapshot, results, body) - window.dispose() + Info_Dockable(view, current_rendering.snapshot, current_results, current_body) + window.dismiss } } - private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) { - background = rendering.tooltip_color - } + private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) window.add(controls.peer, BorderLayout.NORTH) - /* window geometry */ + /* init */ - val screen_point = new Point(mouse_x, mouse_y) - SwingUtilities.convertPointToScreen(screen_point, parent) - val screen_bounds = JEdit_Lib.screen_bounds(screen_point) - + def init( + rendering: Rendering, + mouse_x: Int, mouse_y: Int, + results: Command.Results, + body: XML.Body) { - 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) + current_rendering = rendering + current_results = results + current_body = body + + pretty_text_area.resize(Rendering.font_family(), + Rendering.font_size("jedit_tooltip_font_scale").round) + pretty_text_area.update(rendering.snapshot, results, body) + + content_panel.setBackground(rendering.tooltip_color) + controls.background = rendering.tooltip_color + + + /* window geometry */ + + val screen_point = new Point(mouse_x, mouse_y) + SwingUtilities.convertPointToScreen(screen_point, parent) + val screen_bounds = JEdit_Lib.screen_bounds(screen_point) - 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 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) + + if (window.getWidth == 0) { + window.setSize(new Dimension(100, 100)) + window.setPreferredSize(new Dimension(100, 100)) + } + window.pack + window.revalidate + + val deco_width = window.getWidth - painter.getWidth + val deco_height = window.getHeight - painter.getHeight - val bounds = rendering.tooltip_bounds - 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 + val bounds = rendering.tooltip_bounds + 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 + 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) - window.setLocation(x, y) + 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) + window.setLocation(x, y) + } + + window.setVisible(true) + pretty_text_area.requestFocus + pretty_text_area.refresh() } - window.setVisible(true) - pretty_text_area.requestFocus - pretty_text_area.refresh() + + /* dismiss */ + + def dismiss + { + Swing_Thread.require() + Pretty_Tooltip.dismissed + window.dispose + } } diff -r b041137f7fe5 -r d2bc229e1f37 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 18 12:31:13 2013 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 18 13:18:42 2013 +0100 @@ -190,8 +190,10 @@ } else active_reset() - tooltip_event = Some(e) - tooltip_delay.invoke() + if (Pretty_Tooltip.is_active) { + tooltip_event = Some(e) + tooltip_delay.invoke() + } } } } @@ -220,7 +222,7 @@ 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) + Pretty_Tooltip(view, painter, rendering, x, y1, results, tip) } } }