1.1 --- a/src/Tools/jEdit/etc/options	Sat Dec 15 20:05:53 2012 +0100
     1.2 +++ b/src/Tools/jEdit/etc/options	Sat Dec 15 21:07:52 2012 +0100
     1.3 @@ -12,6 +12,9 @@
     1.4  option jedit_tooltip_margin : int = 60
     1.5    -- "margin for tooltip pretty-printing"
     1.6  
     1.7 +option jedit_tooltip_bounds : real = 0.5
     1.8 +  -- "relative bounds of tooltip window wrt. logical screen size"
     1.9 +
    1.10  option jedit_text_overview_limit : int = 100000
    1.11    -- "maximum amount of text to visualize in overview column"
    1.12  

     2.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Sat Dec 15 20:05:53 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Sat Dec 15 21:07:52 2012 +0100
     2.3 @@ -41,8 +41,8 @@
     2.4  {
     2.5    // FIXME avoid hard-wired stuff
     2.6    private val relevant_options =
     2.7 -    Set("jedit_logic", "jedit_font_scale", "jedit_text_overview_limit",
     2.8 -      "jedit_tooltip_font_scale", "jedit_symbols_search_limit", "jedit_tooltip_margin",
     2.9 +    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
    2.10 +      "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
    2.11        "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
    2.12        "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
    2.13        "editor_tracing_messages", "editor_update_delay")

     3.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Dec 15 20:05:53 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Dec 15 21:07:52 2012 +0100
     3.3 @@ -9,7 +9,7 @@
     3.4  
     3.5  import isabelle._
     3.6  
     3.7 -import java.awt.{Component, Container, Frame, Window}
     3.8 +import java.awt.{Component, Container, Frame, Window, GraphicsEnvironment, Point, Rectangle}
     3.9  
    3.10  import scala.annotation.tailrec
    3.11  
    3.12 @@ -20,6 +20,19 @@
    3.13  
    3.14  object JEdit_Lib
    3.15  {
    3.16 +  /* bounds within multi-screen environment */
    3.17 +
    3.18 +  def screen_bounds(screen_point: Point): Rectangle =
    3.19 +  {
    3.20 +    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
    3.21 +    (for {
    3.22 +      device <- ge.getScreenDevices.iterator
    3.23 +      config <- device.getConfigurations.iterator
    3.24 +      bounds = config.getBounds
    3.25 +    } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
    3.26 +  }
    3.27 +
    3.28 +
    3.29    /* GUI components */
    3.30  
    3.31    def get_parent(component: Component): Option[Container] =

     4.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Dec 15 20:05:53 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Dec 15 21:07:52 2012 +0100
     4.3 @@ -9,7 +9,7 @@
     4.4  
     4.5  import isabelle._
     4.6  
     4.7 -import java.awt.{Toolkit, Color, Point, BorderLayout, Window, Dimension}
     4.8 +import java.awt.{Color, Point, BorderLayout, Window, Dimension}
     4.9  import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
    4.10  import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
    4.11  import javax.swing.border.LineBorder
    4.12 @@ -107,27 +107,27 @@
    4.13  
    4.14    /* window geometry */
    4.15  
    4.16 +  val screen_point = new Point(mouse_x, mouse_y)
    4.17 +  SwingUtilities.convertPointToScreen(screen_point, parent)
    4.18 +  val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
    4.19 +
    4.20    {
    4.21      val font_metrics = pretty_text_area.getPainter.getFontMetrics
    4.22 -    val margin = PIDE.options.int("jedit_tooltip_margin")  // FIXME via rendering?!
    4.23 +    val margin = rendering.tooltip_margin
    4.24      val lines =
    4.25        XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
    4.26          (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
    4.27  
    4.28 -    val screen = Toolkit.getDefaultToolkit.getScreenSize
    4.29 -    val w = (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen.width / 2)
    4.30 -    val h = (font_metrics.getHeight * (lines + 2)) min (screen.height / 2)
    4.31 +    val bounds = rendering.tooltip_bounds
    4.32 +    val w =
    4.33 +      (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen_bounds.width * bounds).toInt
    4.34 +    val h =
    4.35 +      (font_metrics.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt
    4.36      pretty_text_area.setPreferredSize(new Dimension(w, h))
    4.37      window.pack
    4.38 -  }
    4.39  
    4.40 -  {
    4.41 -    val point = new Point(mouse_x, mouse_y)
    4.42 -    SwingUtilities.convertPointToScreen(point, parent)
    4.43 -
    4.44 -    val screen = Toolkit.getDefaultToolkit.getScreenSize
    4.45 -    val x = point.x min (screen.width - window.getWidth)
    4.46 -    val y = point.y min (screen.height - window.getHeight)
    4.47 +    val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
    4.48 +    val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
    4.49      window.setLocation(x, y)
    4.50    }
    4.51  

     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 20:05:53 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 21:07:52 2012 +0100
     5.3 @@ -346,6 +346,9 @@
     5.4      Library.separate(Pretty.FBreak, all_tips.toList)
     5.5    }
     5.6  
     5.7 +  val tooltip_margin: Int = options.int("jedit_tooltip_margin")
     5.8 +  val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8
     5.9 +
    5.10  
    5.11    def gutter_message(range: Text.Range): Option[Icon] =
    5.12    {