# HG changeset patch
# User wenzelm
# Date 1608584180 -3600
# Node ID 3afd293347cce47bcc622d245de298d63e190cb2
# Parent  fc69884a6e5a9f5b146eafb655161a5d64a45196
clarified modules;

diff -r fc69884a6e5a -r 3afd293347cc src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Mon Dec 21 21:53:12 2020 +0100
+++ b/src/Pure/GUI/gui.scala	Mon Dec 21 21:56:20 2020 +0100
@@ -6,16 +6,13 @@
 
 package isabelle
 
-import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException}
-import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
-import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
+import java.awt.{Component, Container, Font, Image, KeyboardFocusManager, Window, Point,
+  Rectangle, Dimension, GraphicsEnvironment, MouseInfo}
+import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
 import java.awt.geom.AffineTransform
-import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
-  JButton, JTextField, JLabel}
-
-
-import scala.collection.JavaConverters
-import scala.swing.{ComboBox, TextArea, ScrollPane}
+import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
+  JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities}
+import scala.swing.{ComboBox, ScrollPane, TextArea}
 import scala.swing.event.SelectionChanged
 
 
@@ -161,6 +158,48 @@
   def isabelle_image(): Image = isabelle_icon().getImage
 
 
+  /* 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
+
+      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)
+    if (component != null) SwingUtilities.convertPointToScreen(screen_point, component)
+
+    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
+    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)
+  }
+
+  def mouse_location(): Screen_Location =
+    screen_location(null, MouseInfo.getPointerInfo.getLocation)
+
+
   /* component hierachy */
 
   def get_parent(component: Component): Option[Container] =
diff -r fc69884a6e5a -r 3afd293347cc src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Dec 21 21:53:12 2020 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Dec 21 21:56:20 2020 +0100
@@ -685,7 +685,7 @@
 
   private val popup =
   {
-    val screen = JEdit_Lib.screen_location(layered, location)
+    val screen = GUI.screen_location(layered, location)
     val size =
     {
       val geometry = JEdit_Lib.window_geometry(completion, completion)
diff -r fc69884a6e5a -r 3afd293347cc src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 21 21:53:12 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 21 21:56:20 2020 +0100
@@ -31,45 +31,6 @@
     (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_))
 
 
-  /* 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
-
-      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
-    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)
-  }
-
-
   /* window geometry measurement */
 
   private lazy val dummy_window = new JWindow
diff -r fc69884a6e5a -r 3afd293347cc src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Dec 21 21:53:12 2020 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Dec 21 21:56:20 2020 +0100
@@ -243,7 +243,7 @@
 
   private val popup =
   {
-    val screen = JEdit_Lib.screen_location(layered, location)
+    val screen = GUI.screen_location(layered, location)
     val size =
     {
       val bounds = JEdit_Rendering.popup_bounds