# HG changeset patch # User wenzelm # Date 1377700606 -7200 # Node ID bd595338ca1802b0b27098e6911502b321cda6e4 # Parent 8d34caf5bf8211c81b5d469598a5cdd90e16513c uniform use of isabelle.jEdit.Popup, based on generic screen location operations; diff -r 8d34caf5bf82 -r bd595338ca18 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Wed Aug 28 15:14:58 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Wed Aug 28 16:36:46 2013 +0200 @@ -249,41 +249,16 @@ private val popup = { - val screen_point = new Point(location.x, location.y) - SwingUtilities.convertPointToScreen(screen_point, layered) - val screen_bounds = JEdit_Lib.screen_bounds(screen_point) - - val w0 = layered.getWidth - val h0 = layered.getHeight - - val (w, h) = + val screen = JEdit_Lib.screen_location(layered, location) + val size = { val geometry = JEdit_Lib.window_geometry(completion, completion) val bounds = Rendering.popup_bounds - val w = geometry.width min (screen_bounds.width * bounds).toInt min w0 - val h = geometry.height min (screen_bounds.height * bounds).toInt min h0 - (w, h) + val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth + val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight + new Dimension(w, h) } - - val (x, y) = - { - val x0 = layered.getLocationOnScreen.x - val y0 = layered.getLocationOnScreen.y - val x1 = x0 + w0 - w - val y1 = y0 + h0 - h - val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w) - val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h) - - val point = new Point((x2 min x1) max x0, (y2 min y1) max y0) - SwingUtilities.convertPointFromScreen(point, layered) - (point.x, point.y) - } - - completion.setLocation(x, y) - completion.setSize(new Dimension(w, h)) - completion.setPreferredSize(new Dimension(w, h)) - - new Popup(layered, completion) + new Popup(layered, completion, screen.relative(layered, size), size) } private def show_popup() diff -r 8d34caf5bf82 -r bd595338ca18 src/Tools/jEdit/src/graphview_dockable.scala --- a/src/Tools/jEdit/src/graphview_dockable.scala Wed Aug 28 15:14:58 2013 +0200 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Aug 28 16:36:46 2013 +0200 @@ -9,7 +9,7 @@ import isabelle._ -import javax.swing.{SwingUtilities, JComponent} +import javax.swing.JComponent import java.awt.Point import java.awt.event.{WindowFocusListener, WindowEvent} @@ -66,10 +66,8 @@ Pretty_Tooltip.invoke(() => { val rendering = Rendering(snapshot, PIDE.options.value) - val screen_point = new Point(x, y) - SwingUtilities.convertPointToScreen(screen_point, parent) val info = Text.Info(Text.Range(~1), body) - Pretty_Tooltip(view, parent, rendering, screen_point, Command.Results.empty, info) + Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info) }) null } diff -r 8d34caf5bf82 -r bd595338ca18 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Wed Aug 28 15:14:58 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Wed Aug 28 16:36:46 2013 +0200 @@ -9,9 +9,9 @@ import isabelle._ -import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle} +import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle, Dimension} import java.awt.event.{KeyEvent, KeyListener} -import javax.swing.{Icon, ImageIcon, JWindow} +import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities} import scala.annotation.tailrec @@ -23,16 +23,42 @@ object JEdit_Lib { - /* bounds within multi-screen environment */ + /* location within multi-screen environment */ + + final case class Screen_Location(point: Point, bounds: Rectangle) + { + def relative(parent: Component, size: Dimension): Point = + { + val w = size.width + val h = size.height - def screen_bounds(screen_point: Point): Rectangle = + val x0 = parent.getLocationOnScreen.x + val y0 = parent.getLocationOnScreen.y + val x1 = x0 + parent.getWidth - w + val y1 = y0 + parent.getHeight - h + val x2 = point.x min (bounds.x + bounds.width - w) + val y2 = point.y min (bounds.y + bounds.height - h) + + val location = new Point((x2 min x1) max x0, (y2 min y1) max y0) + SwingUtilities.convertPointFromScreen(location, parent) + location + } + } + + def screen_location(component: Component, point: Point): Screen_Location = { + val screen_point = new Point(point.x, point.y) + SwingUtilities.convertPointToScreen(screen_point, component) + val ge = GraphicsEnvironment.getLocalGraphicsEnvironment - (for { - device <- ge.getScreenDevices.iterator - config <- device.getConfigurations.iterator - bounds = config.getBounds - } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds + val screen_bounds = + (for { + device <- ge.getScreenDevices.iterator + config <- device.getConfigurations.iterator + bounds = config.getBounds + } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds + + Screen_Location(screen_point, screen_bounds) } diff -r 8d34caf5bf82 -r bd595338ca18 src/Tools/jEdit/src/popup.scala --- a/src/Tools/jEdit/src/popup.scala Wed Aug 28 15:14:58 2013 +0200 +++ b/src/Tools/jEdit/src/popup.scala Wed Aug 28 16:36:46 2013 +0200 @@ -1,7 +1,7 @@ /* Title: Tools/jEdit/src/popup.scala Author: Makarius -Simple popup within layered pane, based on component with given geometry. +Popup within layered pane. */ package isabelle.jedit @@ -9,17 +9,24 @@ import isabelle._ +import java.awt.{Point, Dimension} import javax.swing.{JLayeredPane, JComponent} class Popup( layered: JLayeredPane, - component: JComponent) extends javax.swing.Popup() + component: JComponent, + location: Point, + size: Dimension) extends javax.swing.Popup() { override def show { + component.setLocation(location) + component.setSize(size) + component.setPreferredSize(size) component.setOpaque(true) layered.add(component, JLayeredPane.POPUP_LAYER) + layered.moveToFront(component) layered.repaint(component.getBounds()) } diff -r 8d34caf5bf82 -r bd595338ca18 src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Aug 28 15:14:58 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Wed Aug 28 16:36:46 2013 +0200 @@ -1,7 +1,7 @@ /* Title: Tools/jEdit/src/pretty_tooltip.scala Author: Makarius -Enhanced tooltip window based on Pretty_Text_Area. +Tooltip based on Pretty_Text_Area. */ package isabelle.jedit @@ -11,7 +11,7 @@ import java.awt.{Color, Point, BorderLayout, Dimension} import java.awt.event.{FocusAdapter, FocusEvent} -import javax.swing.{JPanel, JComponent, PopupFactory} +import javax.swing.{JPanel, JComponent, SwingUtilities} import javax.swing.border.LineBorder import scala.swing.{FlowPanel, Label} @@ -39,8 +39,8 @@ def apply( view: View, parent: JComponent, + location: Point, rendering: Rendering, - screen_point: Point, results: Command.Results, info: Text.Info[XML.Body]): Pretty_Tooltip = { @@ -56,7 +56,8 @@ } old.foreach(_.hide_popup) - val tip = new Pretty_Tooltip(view, rendering, screen_point, results, info) + val loc = SwingUtilities.convertPoint(parent, location, view.getLayeredPane) + val tip = new Pretty_Tooltip(view, loc, rendering, results, info) stack = tip :: rest tip.show_popup tip @@ -138,8 +139,8 @@ class Pretty_Tooltip private( view: View, + location: Point, rendering: Rendering, - screen_point: Point, private val results: Command.Results, private val info: Text.Info[XML.Body]) extends JPanel(new BorderLayout) { @@ -217,15 +218,9 @@ private val popup = { - val screen_bounds = JEdit_Lib.screen_bounds(screen_point) - - val root = view.getRootPane - val x0 = root.getLocationOnScreen.x - val y0 = root.getLocationOnScreen.y - val w0 = root.getWidth - val h0 = root.getHeight - - val (w, h) = + val layered = view.getLayeredPane + val screen = JEdit_Lib.screen_location(layered, location) + val size = { val painter = pretty_text_area.getPainter val metric = JEdit_Lib.pretty_metric(painter) @@ -239,8 +234,9 @@ val geometry = JEdit_Lib.window_geometry(tip, tip.pretty_text_area.getPainter) val bounds = Rendering.popup_bounds + val h0 = layered.getHeight val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height - val h2 = h0 min (screen_bounds.height * bounds).toInt + val h2 = h0 min (screen.bounds.height * bounds).toInt val h = h1 min h2 val margin1 = @@ -248,25 +244,14 @@ (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) }) else margin + val w0 = layered.getWidth val w1 = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width - val w2 = w0 min (screen_bounds.width * bounds).toInt + val w2 = w0 min (screen.bounds.width * bounds).toInt val w = w1 min w2 - (w, h) + new Dimension(w, h) } - - val (x, y) = - { - val x1 = x0 + w0 - w - val y1 = y0 + h0 - h - val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w) - val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h) - ((x2 min x1) max x0, (y2 min y1) max y0) - } - - tip.setSize(new Dimension(w, h)) - tip.setPreferredSize(new Dimension(w, h)) - PopupFactory.getSharedInstance.getPopup(root, tip, x, y) + new Popup(layered, tip, screen.relative(layered, size), size) } private def show_popup diff -r 8d34caf5bf82 -r bd595338ca18 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Wed Aug 28 15:14:58 2013 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Aug 28 16:36:46 2013 +0200 @@ -208,10 +208,9 @@ case None => case Some(tip) => val painter = text_area.getPainter - val screen_point = evt.getLocationOnScreen - screen_point.translate(0, painter.getFontMetrics.getHeight / 2) + val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2) val results = rendering.command_results(range) - Pretty_Tooltip(view, painter, rendering, screen_point, results, tip) + Pretty_Tooltip(view, painter, loc, rendering, results, tip) } } }