# HG changeset patch
# User wenzelm
# Date 1355602072 -3600
# Node ID 0493efcc97e9a7494c9c4b176b0d84233e5fad87
# Parent  ce0398b766ce8189da0a3b76f2e78cf293efcdd4
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
more tooltip options via Rendering;

diff -r ce0398b766ce -r 0493efcc97e9 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sat Dec 15 20:05:53 2012 +0100
+++ b/src/Tools/jEdit/etc/options	Sat Dec 15 21:07:52 2012 +0100
@@ -12,6 +12,9 @@
 option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
+option jedit_tooltip_bounds : real = 0.5
+  -- "relative bounds of tooltip window wrt. logical screen size"
+
 option jedit_text_overview_limit : int = 100000
   -- "maximum amount of text to visualize in overview column"
 
diff -r ce0398b766ce -r 0493efcc97e9 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Sat Dec 15 20:05:53 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Sat Dec 15 21:07:52 2012 +0100
@@ -41,8 +41,8 @@
 {
   // FIXME avoid hard-wired stuff
   private val relevant_options =
-    Set("jedit_logic", "jedit_font_scale", "jedit_text_overview_limit",
-      "jedit_tooltip_font_scale", "jedit_symbols_search_limit", "jedit_tooltip_margin",
+    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
+      "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
       "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
       "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
       "editor_tracing_messages", "editor_update_delay")
diff -r ce0398b766ce -r 0493efcc97e9 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Dec 15 20:05:53 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Dec 15 21:07:52 2012 +0100
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.awt.{Component, Container, Frame, Window}
+import java.awt.{Component, Container, Frame, Window, GraphicsEnvironment, Point, Rectangle}
 
 import scala.annotation.tailrec
 
@@ -20,6 +20,19 @@
 
 object JEdit_Lib
 {
+  /* bounds within multi-screen environment */
+
+  def screen_bounds(screen_point: Point): Rectangle =
+  {
+    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
+    (for {
+      device <- ge.getScreenDevices.iterator
+      config <- device.getConfigurations.iterator
+      bounds = config.getBounds
+    } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
+  }
+
+
   /* GUI components */
 
   def get_parent(component: Component): Option[Container] =
diff -r ce0398b766ce -r 0493efcc97e9 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Dec 15 20:05:53 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Dec 15 21:07:52 2012 +0100
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.awt.{Toolkit, Color, Point, BorderLayout, Window, Dimension}
+import java.awt.{Color, Point, BorderLayout, Window, Dimension}
 import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
 import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
 import javax.swing.border.LineBorder
@@ -107,27 +107,27 @@
 
   /* window geometry */
 
+  val screen_point = new Point(mouse_x, mouse_y)
+  SwingUtilities.convertPointToScreen(screen_point, parent)
+  val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
+
   {
     val font_metrics = pretty_text_area.getPainter.getFontMetrics
-    val margin = PIDE.options.int("jedit_tooltip_margin")  // FIXME via rendering?!
+    val margin = rendering.tooltip_margin
     val lines =
       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 + 2)) min (screen.width / 2)
-    val h = (font_metrics.getHeight * (lines + 2)) min (screen.height / 2)
+    val bounds = rendering.tooltip_bounds
+    val w =
+      (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen_bounds.width * bounds).toInt
+    val h =
+      (font_metrics.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt
     pretty_text_area.setPreferredSize(new Dimension(w, h))
     window.pack
-  }
 
-  {
-    val point = new Point(mouse_x, mouse_y)
-    SwingUtilities.convertPointToScreen(point, parent)
-
-    val screen = Toolkit.getDefaultToolkit.getScreenSize
-    val x = point.x min (screen.width - window.getWidth)
-    val y = point.y min (screen.height - window.getHeight)
+    val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
+    val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
     window.setLocation(x, y)
   }
 
diff -r ce0398b766ce -r 0493efcc97e9 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 20:05:53 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 21:07:52 2012 +0100
@@ -346,6 +346,9 @@
     Library.separate(Pretty.FBreak, all_tips.toList)
   }
 
+  val tooltip_margin: Int = options.int("jedit_tooltip_margin")
+  val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8
+
 
   def gutter_message(range: Text.Range): Option[Icon] =
   {