src/Tools/jEdit/src/pretty_tooltip.scala
author wenzelm
Sat, 13 Oct 2012 00:08:36 +0200
changeset 49844 19ea3242ec37
parent 49842 a974f66062c8
child 50146 03f38212442a
permissions -rw-r--r--
improved adhoc height for small fonts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49702
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/pretty_tooltip.scala
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
     3
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
     4
Enhanced tooltip window based on Pretty_Text_Area.
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
     5
*/
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
     6
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
     8
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
     9
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    10
import isabelle._
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    11
49712
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    12
import java.awt.{Toolkit, Color, Point, BorderLayout, Window}
49705
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
    13
import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
    14
import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
49702
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    15
import javax.swing.border.LineBorder
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    16
49725
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    17
import scala.swing.{FlowPanel, Label}
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    18
import scala.swing.event.MouseClicked
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    19
49702
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    20
import org.gjt.sp.jedit.View
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    21
import org.gjt.sp.jedit.textarea.TextArea
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    22
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    23
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    24
class Pretty_Tooltip(
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    25
  view: View,
49730
e0d98ff3c0db use Pretty_Tooltip for Graphview_Panel;
wenzelm
parents: 49728
diff changeset
    26
  parent: JComponent,
49702
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    27
  rendering: Isabelle_Rendering,
49710
21d88a631fcc refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents: 49709
diff changeset
    28
  mouse_x: Int, mouse_y: Int, body: XML.Body)
49730
e0d98ff3c0db use Pretty_Tooltip for Graphview_Panel;
wenzelm
parents: 49728
diff changeset
    29
  extends JWindow(JEdit_Lib.parent_window(parent) getOrElse view)
49702
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    30
{
49705
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
    31
  window =>
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
    32
49725
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    33
  Swing_Thread.require()
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    34
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    35
49705
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
    36
  window.addWindowFocusListener(new WindowAdapter {
49712
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    37
    override def windowLostFocus(e: WindowEvent) {
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    38
      if (!Window.getWindows.exists(w =>
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    39
            w.isDisplayable && JEdit_Lib.ancestors(w).exists(_ == window)))
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    40
        window.dispose()
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    41
    }
49702
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    42
  })
49705
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
    43
49728
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    44
  private val action_listener = new ActionListener {
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    45
    def actionPerformed(e: ActionEvent) {
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    46
      e.getActionCommand match {
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    47
        case "close_all" =>
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    48
          Window.getWindows foreach {
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    49
            case c: Pretty_Tooltip => c.dispose
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    50
            case _ =>
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    51
          }
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    52
        case _ =>
49705
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
    53
      }
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
    54
    }
49728
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    55
  }
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    56
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    57
  window.setContentPane(new JPanel(new BorderLayout) {
49842
a974f66062c8 more uniform tooltip color;
wenzelm
parents: 49730
diff changeset
    58
    setBackground(rendering.tooltip_color)
49728
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    59
    registerKeyboardAction(action_listener, "close_all",
49705
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
    60
      KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
    61
49702
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    62
    override def getFocusTraversalKeysEnabled(): Boolean = false
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    63
  })
49705
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
    64
  window.getRootPane.setBorder(new LineBorder(Color.BLACK))
49702
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
    65
49725
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    66
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    67
  /* pretty text area */
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    68
49703
c89fffb11769 some re-ordering of initialization to ensure proper formatting;
wenzelm
parents: 49702
diff changeset
    69
  val pretty_text_area = new Pretty_Text_Area(view)
49706
92ef8b638c6c tuned color and font size;
wenzelm
parents: 49705
diff changeset
    70
  pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
49703
c89fffb11769 some re-ordering of initialization to ensure proper formatting;
wenzelm
parents: 49702
diff changeset
    71
  pretty_text_area.resize(
c89fffb11769 some re-ordering of initialization to ensure proper formatting;
wenzelm
parents: 49702
diff changeset
    72
    Isabelle.font_family(), Isabelle.font_size("jedit_tooltip_font_scale").round)
c89fffb11769 some re-ordering of initialization to ensure proper formatting;
wenzelm
parents: 49702
diff changeset
    73
  pretty_text_area.update(rendering.snapshot, body)
c89fffb11769 some re-ordering of initialization to ensure proper formatting;
wenzelm
parents: 49702
diff changeset
    74
49728
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    75
  pretty_text_area.registerKeyboardAction(action_listener, "close_all",
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    76
      KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
74f36dab2b62 close tooltips more thoroughly;
wenzelm
parents: 49727
diff changeset
    77
49706
92ef8b638c6c tuned color and font size;
wenzelm
parents: 49705
diff changeset
    78
  window.add(pretty_text_area)
49708
295ec55e7baa tuned window position;
wenzelm
parents: 49707
diff changeset
    79
49725
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    80
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    81
  /* controls */
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
    82
49727
2fe56b600698 make buttons closer to original mouse position;
wenzelm
parents: 49726
diff changeset
    83
  private val close = new Label {
2fe56b600698 make buttons closer to original mouse position;
wenzelm
parents: 49726
diff changeset
    84
    icon = Isabelle_Rendering.tooltip_close_icon
2fe56b600698 make buttons closer to original mouse position;
wenzelm
parents: 49726
diff changeset
    85
    tooltip = "Close tooltip window"
2fe56b600698 make buttons closer to original mouse position;
wenzelm
parents: 49726
diff changeset
    86
    listenTo(mouse.clicks)
2fe56b600698 make buttons closer to original mouse position;
wenzelm
parents: 49726
diff changeset
    87
    reactions += { case _: MouseClicked => window.dispose() }
2fe56b600698 make buttons closer to original mouse position;
wenzelm
parents: 49726
diff changeset
    88
  }
2fe56b600698 make buttons closer to original mouse position;
wenzelm
parents: 49726
diff changeset
    89
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49725
diff changeset
    90
  private val detach = new Label {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49725
diff changeset
    91
    icon = Isabelle_Rendering.tooltip_detach_icon
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49725
diff changeset
    92
    tooltip = "Detach tooltip window"
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49725
diff changeset
    93
    listenTo(mouse.clicks)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49725
diff changeset
    94
    reactions += {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49725
diff changeset
    95
      case _: MouseClicked => Info_Dockable(view, rendering.snapshot, body); window.dispose()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49725
diff changeset
    96
    }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49725
diff changeset
    97
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49725
diff changeset
    98
49842
a974f66062c8 more uniform tooltip color;
wenzelm
parents: 49730
diff changeset
    99
  private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) {
a974f66062c8 more uniform tooltip color;
wenzelm
parents: 49730
diff changeset
   100
    background = rendering.tooltip_color
a974f66062c8 more uniform tooltip color;
wenzelm
parents: 49730
diff changeset
   101
  }
49725
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
   102
  window.add(controls.peer, BorderLayout.NORTH)
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
   103
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
   104
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
   105
  /* window geometry */
f8eeff667076 explicit close button;
wenzelm
parents: 49712
diff changeset
   106
49708
295ec55e7baa tuned window position;
wenzelm
parents: 49707
diff changeset
   107
  {
49707
e42f60561aa4 determine window size from content;
wenzelm
parents: 49706
diff changeset
   108
    val font_metrics = pretty_text_area.getPainter.getFontMetrics
e42f60561aa4 determine window size from content;
wenzelm
parents: 49706
diff changeset
   109
    val margin = Isabelle.options.int("jedit_tooltip_margin")  // FIXME via rendering?!
e42f60561aa4 determine window size from content;
wenzelm
parents: 49706
diff changeset
   110
    val lines =  // FIXME avoid redundant formatting
e42f60561aa4 determine window size from content;
wenzelm
parents: 49706
diff changeset
   111
      XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
e42f60561aa4 determine window size from content;
wenzelm
parents: 49706
diff changeset
   112
        (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
e42f60561aa4 determine window size from content;
wenzelm
parents: 49706
diff changeset
   113
e42f60561aa4 determine window size from content;
wenzelm
parents: 49706
diff changeset
   114
    val screen = Toolkit.getDefaultToolkit.getScreenSize
e42f60561aa4 determine window size from content;
wenzelm
parents: 49706
diff changeset
   115
    val w = (font_metrics.charWidth(Pretty.spc) * margin) min (screen.width / 2)
49844
19ea3242ec37 improved adhoc height for small fonts;
wenzelm
parents: 49842
diff changeset
   116
    val h = (font_metrics.getHeight * (lines + 2) + 25) min (screen.height / 2)
49707
e42f60561aa4 determine window size from content;
wenzelm
parents: 49706
diff changeset
   117
    window.setSize(w, h)
e42f60561aa4 determine window size from content;
wenzelm
parents: 49706
diff changeset
   118
  }
49706
92ef8b638c6c tuned color and font size;
wenzelm
parents: 49705
diff changeset
   119
49709
3062937b45b3 tuned window position to fit on screen;
wenzelm
parents: 49708
diff changeset
   120
  {
49730
e0d98ff3c0db use Pretty_Tooltip for Graphview_Panel;
wenzelm
parents: 49728
diff changeset
   121
    val point = new Point(mouse_x, mouse_y)
e0d98ff3c0db use Pretty_Tooltip for Graphview_Panel;
wenzelm
parents: 49728
diff changeset
   122
    SwingUtilities.convertPointToScreen(point, parent)
49709
3062937b45b3 tuned window position to fit on screen;
wenzelm
parents: 49708
diff changeset
   123
3062937b45b3 tuned window position to fit on screen;
wenzelm
parents: 49708
diff changeset
   124
    val screen = Toolkit.getDefaultToolkit.getScreenSize
3062937b45b3 tuned window position to fit on screen;
wenzelm
parents: 49708
diff changeset
   125
    val x = point.x min (screen.width - window.getWidth)
3062937b45b3 tuned window position to fit on screen;
wenzelm
parents: 49708
diff changeset
   126
    val y = point.y min (screen.height - window.getHeight)
3062937b45b3 tuned window position to fit on screen;
wenzelm
parents: 49708
diff changeset
   127
    window.setLocation(x, y)
3062937b45b3 tuned window position to fit on screen;
wenzelm
parents: 49708
diff changeset
   128
  }
3062937b45b3 tuned window position to fit on screen;
wenzelm
parents: 49708
diff changeset
   129
49705
036c9a028dbd close tooltip window on escape;
wenzelm
parents: 49703
diff changeset
   130
  window.setVisible(true)
49707
e42f60561aa4 determine window size from content;
wenzelm
parents: 49706
diff changeset
   131
  pretty_text_area.refresh()  // FIXME avoid redundant formatting
49702
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
   132
}
696e91c0bc80 separate module Pretty_Tooltip;
wenzelm
parents:
diff changeset
   133