src/Pure/GUI/gui.scala
changeset 73038 3b14f7315dd2
parent 73037 473509b160d9
child 73070 7ef8d77ee761
equal deleted inserted replaced
73037:473509b160d9 73038:3b14f7315dd2
   202 
   202 
   203   /* screen size */
   203   /* screen size */
   204 
   204 
   205   sealed case class Screen_Size(bounds: Rectangle, insets: Insets)
   205   sealed case class Screen_Size(bounds: Rectangle, insets: Insets)
   206   {
   206   {
   207     def x0: Int = bounds.x
   207     def full_screen_bounds: Rectangle =
   208     def y0: Int = bounds.y
   208       if (Platform.is_linux) {
   209     def w0: Int = bounds.width
   209         // avoid menu bar and docking areas
   210     def h0: Int = bounds.height
   210         new Rectangle(
   211     def x: Int = x0 + insets.left
   211           bounds.x + insets.left,
   212     def y: Int = y0 + insets.top
   212           bounds.y + insets.top,
   213     def w: Int = w0 - insets.left - insets.right
   213           bounds.width - insets.left - insets.right,
   214     def h: Int = h0 - insets.top - insets.bottom
   214           bounds.height - insets.top - insets.bottom)
       
   215       }
       
   216       else if (Platform.is_macos) {
       
   217         // avoid menu bar, but ignore docking areas
       
   218         new Rectangle(
       
   219           bounds.x,
       
   220           bounds.y + insets.top,
       
   221           bounds.width,
       
   222           bounds.height - insets.top)
       
   223       }
       
   224       else bounds
   215   }
   225   }
   216 
   226 
   217   def screen_size(component: Component): Screen_Size =
   227   def screen_size(component: Component): Screen_Size =
   218   {
   228   {
   219     val config = component.getGraphicsConfiguration
   229     val config = component.getGraphicsConfiguration