uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
authorwenzelm
Wed Aug 28 16:36:46 2013 +0200 (2013-08-28)
changeset 53247bd595338ca18
parent 53246 8d34caf5bf82
child 53248 7a4b4b3b9ecd
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/popup.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 15:14:58 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 16:36:46 2013 +0200
     1.3 @@ -249,41 +249,16 @@
     1.4  
     1.5    private val popup =
     1.6    {
     1.7 -    val screen_point = new Point(location.x, location.y)
     1.8 -    SwingUtilities.convertPointToScreen(screen_point, layered)
     1.9 -    val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
    1.10 -
    1.11 -    val w0 = layered.getWidth
    1.12 -    val h0 = layered.getHeight
    1.13 -
    1.14 -    val (w, h) =
    1.15 +    val screen = JEdit_Lib.screen_location(layered, location)
    1.16 +    val size =
    1.17      {
    1.18        val geometry = JEdit_Lib.window_geometry(completion, completion)
    1.19        val bounds = Rendering.popup_bounds
    1.20 -      val w = geometry.width min (screen_bounds.width * bounds).toInt min w0
    1.21 -      val h = geometry.height min (screen_bounds.height * bounds).toInt min h0
    1.22 -      (w, h)
    1.23 +      val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth
    1.24 +      val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight
    1.25 +      new Dimension(w, h)
    1.26      }
    1.27 -
    1.28 -    val (x, y) =
    1.29 -    {
    1.30 -      val x0 = layered.getLocationOnScreen.x
    1.31 -      val y0 = layered.getLocationOnScreen.y
    1.32 -      val x1 = x0 + w0 - w
    1.33 -      val y1 = y0 + h0 - h
    1.34 -      val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
    1.35 -      val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
    1.36 -
    1.37 -      val point = new Point((x2 min x1) max x0, (y2 min y1) max y0)
    1.38 -      SwingUtilities.convertPointFromScreen(point, layered)
    1.39 -      (point.x, point.y)
    1.40 -    }
    1.41 -
    1.42 -    completion.setLocation(x, y)
    1.43 -    completion.setSize(new Dimension(w, h))
    1.44 -    completion.setPreferredSize(new Dimension(w, h))
    1.45 -
    1.46 -    new Popup(layered, completion)
    1.47 +    new Popup(layered, completion, screen.relative(layered, size), size)
    1.48    }
    1.49  
    1.50    private def show_popup()
     2.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Wed Aug 28 15:14:58 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Wed Aug 28 16:36:46 2013 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  
     2.5  import isabelle._
     2.6  
     2.7 -import javax.swing.{SwingUtilities, JComponent}
     2.8 +import javax.swing.JComponent
     2.9  import java.awt.Point
    2.10  import java.awt.event.{WindowFocusListener, WindowEvent}
    2.11  
    2.12 @@ -66,10 +66,8 @@
    2.13              Pretty_Tooltip.invoke(() =>
    2.14                {
    2.15                  val rendering = Rendering(snapshot, PIDE.options.value)
    2.16 -                val screen_point = new Point(x, y)
    2.17 -                SwingUtilities.convertPointToScreen(screen_point, parent)
    2.18                  val info = Text.Info(Text.Range(~1), body)
    2.19 -                Pretty_Tooltip(view, parent, rendering, screen_point, Command.Results.empty, info)
    2.20 +                Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
    2.21                })
    2.22              null
    2.23            }
     3.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Aug 28 15:14:58 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Aug 28 16:36:46 2013 +0200
     3.3 @@ -9,9 +9,9 @@
     3.4  
     3.5  import isabelle._
     3.6  
     3.7 -import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
     3.8 +import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle, Dimension}
     3.9  import java.awt.event.{KeyEvent, KeyListener}
    3.10 -import javax.swing.{Icon, ImageIcon, JWindow}
    3.11 +import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
    3.12  
    3.13  import scala.annotation.tailrec
    3.14  
    3.15 @@ -23,16 +23,42 @@
    3.16  
    3.17  object JEdit_Lib
    3.18  {
    3.19 -  /* bounds within multi-screen environment */
    3.20 +  /* location within multi-screen environment */
    3.21 +
    3.22 +  final case class Screen_Location(point: Point, bounds: Rectangle)
    3.23 +  {
    3.24 +    def relative(parent: Component, size: Dimension): Point =
    3.25 +    {
    3.26 +      val w = size.width
    3.27 +      val h = size.height
    3.28  
    3.29 -  def screen_bounds(screen_point: Point): Rectangle =
    3.30 +      val x0 = parent.getLocationOnScreen.x
    3.31 +      val y0 = parent.getLocationOnScreen.y
    3.32 +      val x1 = x0 + parent.getWidth - w
    3.33 +      val y1 = y0 + parent.getHeight - h
    3.34 +      val x2 = point.x min (bounds.x + bounds.width - w)
    3.35 +      val y2 = point.y min (bounds.y + bounds.height - h)
    3.36 +
    3.37 +      val location = new Point((x2 min x1) max x0, (y2 min y1) max y0)
    3.38 +      SwingUtilities.convertPointFromScreen(location, parent)
    3.39 +      location
    3.40 +    }
    3.41 +  }
    3.42 +
    3.43 +  def screen_location(component: Component, point: Point): Screen_Location =
    3.44    {
    3.45 +    val screen_point = new Point(point.x, point.y)
    3.46 +    SwingUtilities.convertPointToScreen(screen_point, component)
    3.47 +
    3.48      val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
    3.49 -    (for {
    3.50 -      device <- ge.getScreenDevices.iterator
    3.51 -      config <- device.getConfigurations.iterator
    3.52 -      bounds = config.getBounds
    3.53 -    } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
    3.54 +    val screen_bounds =
    3.55 +      (for {
    3.56 +        device <- ge.getScreenDevices.iterator
    3.57 +        config <- device.getConfigurations.iterator
    3.58 +        bounds = config.getBounds
    3.59 +      } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
    3.60 +
    3.61 +    Screen_Location(screen_point, screen_bounds)
    3.62    }
    3.63  
    3.64  
     4.1 --- a/src/Tools/jEdit/src/popup.scala	Wed Aug 28 15:14:58 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/popup.scala	Wed Aug 28 16:36:46 2013 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  /*  Title:      Tools/jEdit/src/popup.scala
     4.5      Author:     Makarius
     4.6  
     4.7 -Simple popup within layered pane, based on component with given geometry.
     4.8 +Popup within layered pane.
     4.9  */
    4.10  
    4.11  package isabelle.jedit
    4.12 @@ -9,17 +9,24 @@
    4.13  
    4.14  import isabelle._
    4.15  
    4.16 +import java.awt.{Point, Dimension}
    4.17  import javax.swing.{JLayeredPane, JComponent}
    4.18  
    4.19  
    4.20  class Popup(
    4.21    layered: JLayeredPane,
    4.22 -  component: JComponent) extends javax.swing.Popup()
    4.23 +  component: JComponent,
    4.24 +  location: Point,
    4.25 +  size: Dimension) extends javax.swing.Popup()
    4.26  {
    4.27    override def show
    4.28    {
    4.29 +    component.setLocation(location)
    4.30 +    component.setSize(size)
    4.31 +    component.setPreferredSize(size)
    4.32      component.setOpaque(true)
    4.33      layered.add(component, JLayeredPane.POPUP_LAYER)
    4.34 +    layered.moveToFront(component)
    4.35      layered.repaint(component.getBounds())
    4.36    }
    4.37  
     5.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Aug 28 15:14:58 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Aug 28 16:36:46 2013 +0200
     5.3 @@ -1,7 +1,7 @@
     5.4  /*  Title:      Tools/jEdit/src/pretty_tooltip.scala
     5.5      Author:     Makarius
     5.6  
     5.7 -Enhanced tooltip window based on Pretty_Text_Area.
     5.8 +Tooltip based on Pretty_Text_Area.
     5.9  */
    5.10  
    5.11  package isabelle.jedit
    5.12 @@ -11,7 +11,7 @@
    5.13  
    5.14  import java.awt.{Color, Point, BorderLayout, Dimension}
    5.15  import java.awt.event.{FocusAdapter, FocusEvent}
    5.16 -import javax.swing.{JPanel, JComponent, PopupFactory}
    5.17 +import javax.swing.{JPanel, JComponent, SwingUtilities}
    5.18  import javax.swing.border.LineBorder
    5.19  
    5.20  import scala.swing.{FlowPanel, Label}
    5.21 @@ -39,8 +39,8 @@
    5.22    def apply(
    5.23      view: View,
    5.24      parent: JComponent,
    5.25 +    location: Point,
    5.26      rendering: Rendering,
    5.27 -    screen_point: Point,
    5.28      results: Command.Results,
    5.29      info: Text.Info[XML.Body]): Pretty_Tooltip =
    5.30    {
    5.31 @@ -56,7 +56,8 @@
    5.32            }
    5.33          old.foreach(_.hide_popup)
    5.34  
    5.35 -        val tip = new Pretty_Tooltip(view, rendering, screen_point, results, info)
    5.36 +        val loc = SwingUtilities.convertPoint(parent, location, view.getLayeredPane)
    5.37 +        val tip = new Pretty_Tooltip(view, loc, rendering, results, info)
    5.38          stack = tip :: rest
    5.39          tip.show_popup
    5.40          tip
    5.41 @@ -138,8 +139,8 @@
    5.42  
    5.43  class Pretty_Tooltip private(
    5.44    view: View,
    5.45 +  location: Point,
    5.46    rendering: Rendering,
    5.47 -  screen_point: Point,
    5.48    private val results: Command.Results,
    5.49    private val info: Text.Info[XML.Body]) extends JPanel(new BorderLayout)
    5.50  {
    5.51 @@ -217,15 +218,9 @@
    5.52  
    5.53    private val popup =
    5.54    {
    5.55 -    val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
    5.56 -
    5.57 -    val root = view.getRootPane
    5.58 -    val x0 = root.getLocationOnScreen.x
    5.59 -    val y0 = root.getLocationOnScreen.y
    5.60 -    val w0 = root.getWidth
    5.61 -    val h0 = root.getHeight
    5.62 -
    5.63 -    val (w, h) =
    5.64 +    val layered = view.getLayeredPane
    5.65 +    val screen = JEdit_Lib.screen_location(layered, location)
    5.66 +    val size =
    5.67      {
    5.68        val painter = pretty_text_area.getPainter
    5.69        val metric = JEdit_Lib.pretty_metric(painter)
    5.70 @@ -239,8 +234,9 @@
    5.71        val geometry = JEdit_Lib.window_geometry(tip, tip.pretty_text_area.getPainter)
    5.72        val bounds = Rendering.popup_bounds
    5.73  
    5.74 +      val h0 = layered.getHeight
    5.75        val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
    5.76 -      val h2 = h0 min (screen_bounds.height * bounds).toInt
    5.77 +      val h2 = h0 min (screen.bounds.height * bounds).toInt
    5.78        val h = h1 min h2
    5.79  
    5.80        val margin1 =
    5.81 @@ -248,25 +244,14 @@
    5.82            (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
    5.83          else margin
    5.84  
    5.85 +      val w0 = layered.getWidth
    5.86        val w1 = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
    5.87 -      val w2 = w0 min (screen_bounds.width * bounds).toInt
    5.88 +      val w2 = w0 min (screen.bounds.width * bounds).toInt
    5.89        val w = w1 min w2
    5.90  
    5.91 -      (w, h)
    5.92 +      new Dimension(w, h)
    5.93      }
    5.94 -
    5.95 -    val (x, y) =
    5.96 -    {
    5.97 -      val x1 = x0 + w0 - w
    5.98 -      val y1 = y0 + h0 - h
    5.99 -      val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
   5.100 -      val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
   5.101 -      ((x2 min x1) max x0, (y2 min y1) max y0)
   5.102 -    }
   5.103 -
   5.104 -    tip.setSize(new Dimension(w, h))
   5.105 -    tip.setPreferredSize(new Dimension(w, h))
   5.106 -    PopupFactory.getSharedInstance.getPopup(root, tip, x, y)
   5.107 +    new Popup(layered, tip, screen.relative(layered, size), size)
   5.108    }
   5.109  
   5.110    private def show_popup
     6.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Aug 28 15:14:58 2013 +0200
     6.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Aug 28 16:36:46 2013 +0200
     6.3 @@ -208,10 +208,9 @@
     6.4                        case None =>
     6.5                        case Some(tip) =>
     6.6                          val painter = text_area.getPainter
     6.7 -                        val screen_point = evt.getLocationOnScreen
     6.8 -                        screen_point.translate(0, painter.getFontMetrics.getHeight / 2)
     6.9 +                        val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
    6.10                          val results = rendering.command_results(range)
    6.11 -                        Pretty_Tooltip(view, painter, rendering, screen_point, results, tip)
    6.12 +                        Pretty_Tooltip(view, painter, loc, rendering, results, tip)
    6.13                      }
    6.14                  }
    6.15                }