# HG changeset patch
# User wenzelm
# Date 1349429806 -7200
# Node ID e42f60561aa4a76191d66461387a03e86eff8b84
# Parent  92ef8b638c6c760c75ba9ee60d994d384a2f809e
determine window size from content;

diff -r 92ef8b638c6c -r e42f60561aa4 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 11:09:24 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 11:36:46 2012 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.awt.{Color, Point, BorderLayout}
+import java.awt.{Toolkit, Color, Point, BorderLayout}
 import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
 import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
 import javax.swing.border.LineBorder
@@ -63,10 +63,21 @@
 
   window.add(pretty_text_area)
   window.setLocation(point.x, point.y)
-  window.setSize(pretty_text_area.getPainter.getFontMetrics.charWidth(Pretty.spc) *
-    Isabelle.options.int("jedit_tooltip_margin"), 100)
+
+  {
+    val font_metrics = pretty_text_area.getPainter.getFontMetrics
+    val margin = Isabelle.options.int("jedit_tooltip_margin")  // FIXME via rendering?!
+    val lines =  // FIXME avoid redundant formatting
+      XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
+        (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
+
+    val screen = Toolkit.getDefaultToolkit.getScreenSize
+    val w = (font_metrics.charWidth(Pretty.spc) * margin) min (screen.width / 2)
+    val h = (font_metrics.getHeight * (lines + 2)) min (screen.height / 2)
+    window.setSize(w, h)
+  }
 
   window.setVisible(true)
-  pretty_text_area.refresh()
+  pretty_text_area.refresh()  // FIXME avoid redundant formatting
 }