# HG changeset patch # User wenzelm # Date 1376416332 -7200 # Node ID afdabfeb5e940009e5a2f478786b06783cdaf91b # Parent 0f376701e83bddd212e893777792895dcef3894e# Parent be9e94594b9612eba3b44db4b83bc271c7f218be merged diff -r 0f376701e83b -r afdabfeb5e94 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Tue Aug 13 17:45:22 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Aug 13 19:52:12 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] = diff -r 0f376701e83b -r afdabfeb5e94 src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Tue Aug 13 17:45:22 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Tue Aug 13 19:52:12 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)