# HG changeset patch
# User wenzelm
# Date 1349431883 -7200
# Node ID 3062937b45b3afbabf91ce29fdc84a0ebee4fa3b
# Parent  295ec55e7baa73bb873fc7eff41e20bc9dcdcc2a
tuned window position to fit on screen;

diff -r 295ec55e7baa -r 3062937b45b3 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 12:00:28 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 12:11:23 2012 +0200
@@ -22,7 +22,7 @@
   view: View,
   text_area: TextArea,
   rendering: Isabelle_Rendering,
-  x: Int, y: Int, body: XML.Body) extends JWindow(view)
+  mouse_x: Int, mouse_y: Int, body: XML.Body) extends JWindow(view)
 {
   window =>
 
@@ -55,14 +55,6 @@
   window.add(pretty_text_area)
 
   {
-    val container = text_area.getPainter
-    val font_metrics = container.getFontMetrics
-    val point = new Point(x, y + font_metrics.getHeight / 2)
-    SwingUtilities.convertPointToScreen(point, container)
-    window.setLocation(point.x, point.y)
-  }
-
-  {
     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
@@ -75,6 +67,18 @@
     window.setSize(w, h)
   }
 
+  {
+    val container = text_area.getPainter
+    val font_metrics = container.getFontMetrics
+    val point = new Point(mouse_x, mouse_y + font_metrics.getHeight / 2)
+    SwingUtilities.convertPointToScreen(point, container)
+
+    val screen = Toolkit.getDefaultToolkit.getScreenSize
+    val x = point.x min (screen.width - window.getWidth)
+    val y = point.y min (screen.height - window.getHeight)
+    window.setLocation(x, y)
+  }
+
   window.setVisible(true)
   pretty_text_area.refresh()  // FIXME avoid redundant formatting
 }