more general window_geometry;

--- 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] =

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Aug 13 16:15:31 2013 +0200
@@ -11,7 +11,7 @@
 
 import java.awt.{Color, Point, BorderLayout, Dimension}
 import java.awt.event.{FocusAdapter, FocusEvent}
-import javax.swing.{JWindow, JPanel, JComponent, PopupFactory}
+import javax.swing.{JPanel, JComponent, PopupFactory}
 import javax.swing.border.LineBorder
 
 import scala.swing.{FlowPanel, Label}
@@ -133,28 +133,6 @@
       true
     }
   }
-
-
-  /* auxiliary geometry measurement */
-
-  private lazy val dummy_window = new JWindow
-
-  private def decoration_size(tip: Pretty_Tooltip): (Int, Int) =
-  {
-    val old_content = dummy_window.getContentPane
-
-    dummy_window.setContentPane(tip)
-    dummy_window.pack
-    dummy_window.revalidate
-
-    val painter = tip.pretty_text_area.getPainter
-    val w = dummy_window.getWidth - painter.getWidth
-    val h = dummy_window.getHeight - painter.getHeight
-
-    dummy_window.setContentPane(old_content)
-
-    (w, h)
-  }
 }
 
 
@@ -253,10 +231,10 @@
         XML.traverse_text(formatted)(0)(
           (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
 
-      val (deco_width, deco_height) = Pretty_Tooltip.decoration_size(tip)
+      val geometry = JEdit_Lib.window_geometry(tip, tip.pretty_text_area.getPainter)
       val bounds = rendering.tooltip_bounds
 
-      val h1 = painter.getFontMetrics.getHeight * (lines + 1) + deco_height
+      val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
       val h2 = (screen_bounds.height * bounds).toInt
       val h = h1 min h2
 
@@ -265,7 +243,7 @@
           (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
         else margin
       val w =
-        ((metric.unit * (margin1 + metric.average)).round.toInt + deco_width) min
+        ((metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width) min
         (screen_bounds.width * bounds).toInt
 
       (w, h)