src/Tools/jEdit/src/pretty_tooltip.scala
author wenzelm
Sat Mar 23 19:39:31 2013 +0100 (2013-03-23 ago)
changeset 51496 cb677987b7e3
parent 51493 59d8a1031c00
child 52472 3a43a8b1ecb0
permissions -rw-r--r--
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
     1 /*  Title:      Tools/jEdit/src/pretty_tooltip.scala
     2     Author:     Makarius
     3 
     4 Enhanced tooltip window based on Pretty_Text_Area.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.{Color, Point, BorderLayout, Window, Dimension}
    13 import java.awt.event.{WindowEvent, WindowAdapter, KeyEvent, KeyAdapter, KeyListener}
    14 import javax.swing.{SwingUtilities, JDialog, JPanel, JComponent}
    15 import javax.swing.border.LineBorder
    16 
    17 import scala.swing.{FlowPanel, Label}
    18 import scala.swing.event.MouseClicked
    19 
    20 import org.gjt.sp.jedit.View
    21 import org.gjt.sp.jedit.textarea.TextArea
    22 
    23 
    24 object Pretty_Tooltip
    25 {
    26   /* window stack -- owned by Swing thread */
    27 
    28   private var window_stack: List[Pretty_Tooltip] = Nil
    29 
    30   def windows(): List[Pretty_Tooltip] =
    31   {
    32     Swing_Thread.require()
    33     window_stack
    34   }
    35 
    36   def apply(
    37     view: View,
    38     parent: JComponent,
    39     rendering: Rendering,
    40     mouse_x: Int, mouse_y: Int,
    41     results: Command.Results,
    42     range: Text.Range,
    43     body: XML.Body): Pretty_Tooltip =
    44   {
    45     Swing_Thread.require()
    46 
    47     val old_windows =
    48       JEdit_Lib.parent_window(parent) match {
    49         case Some(parent_window: Pretty_Tooltip) =>
    50           windows().find(_ == parent_window) match {
    51             case Some(window) => window.descendants()
    52             case None => windows()
    53           }
    54         case _ => windows()
    55       }
    56 
    57     val window =
    58       old_windows.reverse match {
    59         case Nil =>
    60           val window = new Pretty_Tooltip(view)
    61           window_stack = window :: window_stack
    62           window
    63         case window :: others =>
    64           others.foreach(_.dispose)
    65           window
    66       }
    67     window.init(rendering, parent, mouse_x, mouse_y, results, range, body)
    68     window
    69   }
    70 
    71 
    72   /* global dismissed delay -- owned by Swing thread */
    73 
    74   private var active = true
    75 
    76   private lazy val reactivate_delay =
    77     Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
    78       active = true
    79     }
    80 
    81   def dismissed
    82   {
    83     Swing_Thread.require()
    84     active = false
    85     reactivate_delay.invoke()
    86   }
    87 
    88   def is_active: Boolean =
    89   {
    90     Swing_Thread.require()
    91     active
    92   }
    93 }
    94 
    95 
    96 class Pretty_Tooltip private(view: View) extends JDialog
    97 {
    98   window =>
    99 
   100   Swing_Thread.require()
   101 
   102 
   103   /* implicit state -- owned by Swing thread */
   104 
   105   private var current_rendering: Rendering =
   106     Rendering(Document.State.init.snapshot(), PIDE.options.value)
   107   private var current_results = Command.Results.empty
   108   private var current_range = Text.Range(-1)
   109   private var current_body: XML.Body = Nil
   110 
   111 
   112   /* window hierarchy */
   113 
   114   def descendants(): List[Pretty_Tooltip] =
   115     if (Pretty_Tooltip.windows().exists(_ == window))
   116       Pretty_Tooltip.windows().takeWhile(_ != window)
   117     else Nil
   118 
   119   window.addWindowFocusListener(new WindowAdapter {
   120     override def windowLostFocus(e: WindowEvent) {
   121       if (!descendants().exists(_.isDisplayable))
   122         window.dismiss
   123     }
   124   })
   125 
   126 
   127   /* main content */
   128 
   129   window.setUndecorated(true)
   130   window.getRootPane.setBorder(new LineBorder(Color.BLACK))
   131 
   132   private val content_panel =
   133     new JPanel(new BorderLayout) { override def getFocusTraversalKeysEnabled = false }
   134   window.setContentPane(content_panel)
   135 
   136   val pretty_text_area = new Pretty_Text_Area(view, () => window.dismiss, true) {
   137     override def get_background() = Some(current_rendering.tooltip_color)
   138   }
   139   window.add(pretty_text_area)
   140 
   141 
   142   /* controls */
   143 
   144   private val close = new Label {
   145     icon = Rendering.tooltip_close_icon
   146     tooltip = "Close tooltip window"
   147     listenTo(mouse.clicks)
   148     reactions += { case _: MouseClicked => window.dismiss }
   149   }
   150 
   151   private val detach = new Label {
   152     icon = Rendering.tooltip_detach_icon
   153     tooltip = "Detach tooltip window"
   154     listenTo(mouse.clicks)
   155     reactions += {
   156       case _: MouseClicked =>
   157         Info_Dockable(view, current_rendering.snapshot, current_results, current_body)
   158         window.dismiss
   159     }
   160   }
   161 
   162   private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach)
   163   window.add(controls.peer, BorderLayout.NORTH)
   164 
   165 
   166   /* init */
   167 
   168   def init(
   169     rendering: Rendering,
   170     parent: JComponent,
   171     mouse_x: Int, mouse_y: Int,
   172     results: Command.Results,
   173     range: Text.Range,
   174     body: XML.Body)
   175   {
   176     if (!(results == current_results && range == current_range && body == current_body)) {
   177       current_rendering = rendering
   178       current_results = results
   179       current_range = range
   180       current_body = body
   181 
   182       pretty_text_area.resize(Rendering.font_family(),
   183         Rendering.font_size("jedit_tooltip_font_scale").round)
   184       pretty_text_area.update(rendering.snapshot, results, body)
   185 
   186       content_panel.setBackground(rendering.tooltip_color)
   187       controls.background = rendering.tooltip_color
   188 
   189 
   190       /* window geometry */
   191 
   192       val screen_point = new Point(mouse_x, mouse_y)
   193       SwingUtilities.convertPointToScreen(screen_point, parent)
   194       val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
   195 
   196       {
   197         val painter = pretty_text_area.getPainter
   198         val metric = JEdit_Lib.pretty_metric(painter)
   199         val margin = rendering.tooltip_margin * metric.average
   200         val lines =
   201           XML.traverse_text(Pretty.formatted(body, margin, metric))(0)(
   202             (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
   203 
   204         if (window.getWidth == 0) {
   205           window.setSize(new Dimension(100, 100))
   206           window.setPreferredSize(new Dimension(100, 100))
   207         }
   208         window.pack
   209         window.revalidate
   210 
   211         val deco_width = window.getWidth - painter.getWidth
   212         val deco_height = window.getHeight - painter.getHeight
   213 
   214         val bounds = rendering.tooltip_bounds
   215         val w =
   216           ((metric.unit * (margin + metric.average)).round.toInt + deco_width) min
   217           (screen_bounds.width * bounds).toInt
   218         val h =
   219           (painter.getFontMetrics.getHeight * (lines + 1) + deco_height) min
   220           (screen_bounds.height * bounds).toInt
   221 
   222         window.setSize(new Dimension(w, h))
   223         window.setPreferredSize(new Dimension(w, h))
   224         window.pack
   225         window.revalidate
   226 
   227         val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
   228         val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
   229         window.setLocation(x, y)
   230       }
   231     }
   232 
   233     window.setVisible(true)
   234     pretty_text_area.requestFocus
   235     pretty_text_area.refresh()
   236   }
   237 
   238 
   239   /* dismiss */
   240 
   241   def dismiss
   242   {
   243     Swing_Thread.require()
   244     Pretty_Tooltip.dismissed
   245     window.dispose
   246   }
   247 }
   248