src/Tools/jEdit/src/jedit_lib.scala

--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 13 16:15:31 2013 +0200
@@ -10,7 +10,7 @@
 import isabelle._
 
 import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
-import javax.swing.{Icon, ImageIcon}
+import javax.swing.{Icon, ImageIcon, JWindow}
 
 import scala.annotation.tailrec
 
@@ -34,6 +34,36 @@
   }
 
 
+  /* window geometry measurement */
+
+  private lazy val dummy_window = new JWindow
+
+  final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int)
+  {
+    def deco_width: Int = width - inner_width
+    def deco_height: Int = height - inner_height
+  }
+
+  def window_geometry(outer: Container, inner: Component): Window_Geometry =
+  {
+    Swing_Thread.require()
+
+    val old_content = dummy_window.getContentPane
+
+    dummy_window.setContentPane(outer)
+    dummy_window.pack
+    dummy_window.revalidate
+
+    val geometry =
+      Window_Geometry(
+        dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)
+
+    dummy_window.setContentPane(old_content)
+
+    geometry
+  }
+
+
   /* GUI components */
 
   def get_parent(component: Component): Option[Container] =