1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 13 16:15:31 2013 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  import isabelle._
     1.5  
     1.6  import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
     1.7 -import javax.swing.{Icon, ImageIcon}
     1.8 +import javax.swing.{Icon, ImageIcon, JWindow}
     1.9  
    1.10  import scala.annotation.tailrec
    1.11  
    1.12 @@ -34,6 +34,36 @@
    1.13    }
    1.14  
    1.15  
    1.16 +  /* window geometry measurement */
    1.17 +
    1.18 +  private lazy val dummy_window = new JWindow
    1.19 +
    1.20 +  final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int)
    1.21 +  {
    1.22 +    def deco_width: Int = width - inner_width
    1.23 +    def deco_height: Int = height - inner_height
    1.24 +  }
    1.25 +
    1.26 +  def window_geometry(outer: Container, inner: Component): Window_Geometry =
    1.27 +  {
    1.28 +    Swing_Thread.require()
    1.29 +
    1.30 +    val old_content = dummy_window.getContentPane
    1.31 +
    1.32 +    dummy_window.setContentPane(outer)
    1.33 +    dummy_window.pack
    1.34 +    dummy_window.revalidate
    1.35 +
    1.36 +    val geometry =
    1.37 +      Window_Geometry(
    1.38 +        dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)
    1.39 +
    1.40 +    dummy_window.setContentPane(old_content)
    1.41 +
    1.42 +    geometry
    1.43 +  }
    1.44 +
    1.45 +
    1.46    /* GUI components */
    1.47  
    1.48    def get_parent(component: Component): Option[Container] =

     2.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Aug 13 14:20:22 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Aug 13 16:15:31 2013 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4  
     2.5  import java.awt.{Color, Point, BorderLayout, Dimension}
     2.6  import java.awt.event.{FocusAdapter, FocusEvent}
     2.7 -import javax.swing.{JWindow, JPanel, JComponent, PopupFactory}
     2.8 +import javax.swing.{JPanel, JComponent, PopupFactory}
     2.9  import javax.swing.border.LineBorder
    2.10  
    2.11  import scala.swing.{FlowPanel, Label}
    2.12 @@ -133,28 +133,6 @@
    2.13        true
    2.14      }
    2.15    }
    2.16 -
    2.17 -
    2.18 -  /* auxiliary geometry measurement */
    2.19 -
    2.20 -  private lazy val dummy_window = new JWindow
    2.21 -
    2.22 -  private def decoration_size(tip: Pretty_Tooltip): (Int, Int) =
    2.23 -  {
    2.24 -    val old_content = dummy_window.getContentPane
    2.25 -
    2.26 -    dummy_window.setContentPane(tip)
    2.27 -    dummy_window.pack
    2.28 -    dummy_window.revalidate
    2.29 -
    2.30 -    val painter = tip.pretty_text_area.getPainter
    2.31 -    val w = dummy_window.getWidth - painter.getWidth
    2.32 -    val h = dummy_window.getHeight - painter.getHeight
    2.33 -
    2.34 -    dummy_window.setContentPane(old_content)
    2.35 -
    2.36 -    (w, h)
    2.37 -  }
    2.38  }
    2.39  
    2.40  
    2.41 @@ -253,10 +231,10 @@
    2.42          XML.traverse_text(formatted)(0)(
    2.43            (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
    2.44  
    2.45 -      val (deco_width, deco_height) = Pretty_Tooltip.decoration_size(tip)
    2.46 +      val geometry = JEdit_Lib.window_geometry(tip, tip.pretty_text_area.getPainter)
    2.47        val bounds = rendering.tooltip_bounds
    2.48  
    2.49 -      val h1 = painter.getFontMetrics.getHeight * (lines + 1) + deco_height
    2.50 +      val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
    2.51        val h2 = (screen_bounds.height * bounds).toInt
    2.52        val h = h1 min h2
    2.53  
    2.54 @@ -265,7 +243,7 @@
    2.55            (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
    2.56          else margin
    2.57        val w =
    2.58 -        ((metric.unit * (margin1 + metric.average)).round.toInt + deco_width) min
    2.59 +        ((metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width) min
    2.60          (screen_bounds.width * bounds).toInt
    2.61  
    2.62        (w, h)