diff -r b028e8d22d8d -r 473509b160d9 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Sun Jan 03 16:21:59 2021 +0100
+++ b/src/Pure/GUI/gui.scala	Sun Jan 03 22:06:19 2021 +0100
@@ -6,8 +6,8 @@
 
 package isabelle
 
-import java.awt.{Component, Container, Font, Image, KeyboardFocusManager, Window, Point,
-  Rectangle, Dimension, GraphicsEnvironment, MouseInfo}
+import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point,
+  Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit}
 import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
 import java.awt.geom.AffineTransform
 import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
@@ -200,6 +200,29 @@
     screen_location(null, MouseInfo.getPointerInfo.getLocation)
 
 
+  /* screen size */
+
+  sealed case class Screen_Size(bounds: Rectangle, insets: Insets)
+  {
+    def x0: Int = bounds.x
+    def y0: Int = bounds.y
+    def w0: Int = bounds.width
+    def h0: Int = bounds.height
+    def x: Int = x0 + insets.left
+    def y: Int = y0 + insets.top
+    def w: Int = w0 - insets.left - insets.right
+    def h: Int = h0 - insets.top - insets.bottom
+  }
+
+  def screen_size(component: Component): Screen_Size =
+  {
+    val config = component.getGraphicsConfiguration
+    val bounds = config.getBounds
+    val insets = Toolkit.getDefaultToolkit.getScreenInsets(config)
+    Screen_Size(bounds, insets)
+  }
+
+
   /* component hierachy */
 
   def get_parent(component: Component): Option[Container] =