# HG changeset patch
# User wenzelm
# Date 1609711276 -3600
# Node ID 3b14f7315dd2f52fe00e18e6bba7ab129c9c2260
# Parent  473509b160d97e1046df0c604e53fceb7fb94e27
some attempts at multi-platform full-screen mode;

diff -r 473509b160d9 -r 3b14f7315dd2 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Sun Jan 03 22:06:19 2021 +0100
+++ b/src/Pure/GUI/gui.scala	Sun Jan 03 23:01:16 2021 +0100
@@ -204,14 +204,24 @@
 
   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 full_screen_bounds: Rectangle =
+      if (Platform.is_linux) {
+        // avoid menu bar and docking areas
+        new Rectangle(
+          bounds.x + insets.left,
+          bounds.y + insets.top,
+          bounds.width - insets.left - insets.right,
+          bounds.height - insets.top - insets.bottom)
+      }
+      else if (Platform.is_macos) {
+        // avoid menu bar, but ignore docking areas
+        new Rectangle(
+          bounds.x,
+          bounds.y + insets.top,
+          bounds.width,
+          bounds.height - insets.top)
+      }
+      else bounds
   }
 
   def screen_size(component: Component): Screen_Size =