# HG changeset patch
# User wenzelm
# Date 1608587757 -3600
# Node ID e028331c578b5bca7e48de85db66d36f30b24103
# Parent  51442c6dc29633308cbfadb160f476db63bbbb21
clarified window size;

diff -r 51442c6dc296 -r e028331c578b src/Pure/Tools/java_monitor.scala
--- a/src/Pure/Tools/java_monitor.scala	Mon Dec 21 22:47:53 2020 +0100
+++ b/src/Pure/Tools/java_monitor.scala	Mon Dec 21 22:55:57 2020 +0100
@@ -43,8 +43,8 @@
       val jconsole = new JConsole(false)
 
       val screen = GUI.mouse_location()
-      val width = 1200 min screen.bounds.width
-      val height = 900 min screen.bounds.height
+      val width = (1200 max (screen.bounds.width / 2)) min screen.bounds.width
+      val height = (900 max (screen.bounds.height / 2)) min screen.bounds.height
       jconsole.setBounds(
         screen.bounds.x + (screen.bounds.width - width) / 2,
         screen.bounds.y + (screen.bounds.height - height) / 2,