src/Tools/jEdit/src/pretty_tooltip.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64621 7116f2634e32
child 66591 6efa351190d0
permissions -rw-r--r--
tuned signature;
wenzelm@49702
     1
/*  Title:      Tools/jEdit/src/pretty_tooltip.scala
wenzelm@49702
     2
    Author:     Makarius
wenzelm@49702
     3
wenzelm@53247
     4
Tooltip based on Pretty_Text_Area.
wenzelm@49702
     5
*/
wenzelm@49702
     6
wenzelm@49702
     7
package isabelle.jedit
wenzelm@49702
     8
wenzelm@49702
     9
wenzelm@49702
    10
import isabelle._
wenzelm@49702
    11
wenzelm@52478
    12
import java.awt.{Color, Point, BorderLayout, Dimension}
wenzelm@52478
    13
import java.awt.event.{FocusAdapter, FocusEvent}
wenzelm@53778
    14
import javax.swing.{JPanel, JComponent, SwingUtilities, JLayeredPane}
wenzelm@49702
    15
import javax.swing.border.LineBorder
wenzelm@49702
    16
wenzelm@49725
    17
import scala.swing.{FlowPanel, Label}
wenzelm@49725
    18
import scala.swing.event.MouseClicked
wenzelm@49725
    19
wenzelm@49702
    20
import org.gjt.sp.jedit.View
wenzelm@49702
    21
import org.gjt.sp.jedit.textarea.TextArea
wenzelm@49702
    22
wenzelm@49702
    23
wenzelm@51449
    24
object Pretty_Tooltip
wenzelm@51449
    25
{
wenzelm@52478
    26
  /* tooltip hierarchy */
wenzelm@51449
    27
wenzelm@57612
    28
  // owned by GUI thread
wenzelm@52478
    29
  private var stack: List[Pretty_Tooltip] = Nil
wenzelm@51449
    30
wenzelm@52478
    31
  private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] =
wenzelm@51449
    32
  {
wenzelm@57612
    33
    GUI_Thread.require {}
wenzelm@52478
    34
wenzelm@52478
    35
    if (stack.contains(tip)) Some(stack.span(_ != tip))
wenzelm@52478
    36
    else None
wenzelm@51449
    37
  }
wenzelm@51449
    38
wenzelm@56497
    39
  private def descendant(parent: JComponent): Option[Pretty_Tooltip] =
wenzelm@57612
    40
    GUI_Thread.require { stack.find(tip => tip.original_parent == parent) }
wenzelm@56497
    41
wenzelm@51449
    42
  def apply(
wenzelm@51449
    43
    view: View,
wenzelm@51449
    44
    parent: JComponent,
wenzelm@53247
    45
    location: Point,
wenzelm@64621
    46
    rendering: JEdit_Rendering,
wenzelm@51449
    47
    results: Command.Results,
wenzelm@53778
    48
    info: Text.Info[XML.Body])
wenzelm@51449
    49
  {
wenzelm@57612
    50
    GUI_Thread.require {}
wenzelm@51449
    51
wenzelm@52497
    52
    stack match {
wenzelm@53779
    53
      case top :: _ if top.results == results && top.info == info =>
wenzelm@52497
    54
      case _ =>
wenzelm@53778
    55
        GUI.layered_pane(parent) match {
wenzelm@53778
    56
          case None =>
wenzelm@53778
    57
          case Some(layered) =>
wenzelm@53778
    58
            val (old, rest) =
wenzelm@53778
    59
              GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
wenzelm@53778
    60
                case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
wenzelm@53778
    61
                case None => (stack, Nil)
wenzelm@53778
    62
              }
wenzelm@53778
    63
            old.foreach(_.hide_popup)
wenzelm@52497
    64
wenzelm@53778
    65
            val loc = SwingUtilities.convertPoint(parent, location, layered)
wenzelm@56497
    66
            val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info)
wenzelm@53778
    67
            stack = tip :: rest
wenzelm@53778
    68
            tip.show_popup
wenzelm@53778
    69
        }
wenzelm@52496
    70
    }
wenzelm@51449
    71
  }
wenzelm@51452
    72
wenzelm@51452
    73
wenzelm@57612
    74
  /* pending event and active state */  // owned by GUI thread
wenzelm@51452
    75
wenzelm@52494
    76
  private var pending: Option[() => Unit] = None
wenzelm@51452
    77
  private var active = true
wenzelm@52494
    78
wenzelm@52494
    79
  private val pending_delay =
wenzelm@57612
    80
    GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
wenzelm@52494
    81
      pending match {
wenzelm@52494
    82
        case Some(body) => pending = None; body()
wenzelm@52494
    83
        case None =>
wenzelm@52494
    84
      }
wenzelm@52494
    85
    }
wenzelm@51452
    86
wenzelm@52494
    87
  def invoke(body: () => Unit): Unit =
wenzelm@57612
    88
    GUI_Thread.require {
wenzelm@52494
    89
      if (active) {
wenzelm@52494
    90
        pending = Some(body)
wenzelm@52494
    91
        pending_delay.invoke()
wenzelm@52494
    92
      }
wenzelm@52494
    93
    }
wenzelm@52494
    94
wenzelm@52664
    95
  def revoke(): Unit =
wenzelm@57612
    96
    GUI_Thread.require {
wenzelm@52664
    97
      pending = None
wenzelm@52664
    98
      pending_delay.revoke()
wenzelm@52664
    99
    }
wenzelm@52664
   100
wenzelm@51452
   101
  private lazy val reactivate_delay =
wenzelm@57612
   102
    GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
wenzelm@51452
   103
      active = true
wenzelm@51452
   104
    }
wenzelm@51452
   105
wenzelm@52494
   106
  private def deactivate(): Unit =
wenzelm@57612
   107
    GUI_Thread.require {
wenzelm@52664
   108
      revoke()
wenzelm@52494
   109
      active = false
wenzelm@52494
   110
      reactivate_delay.invoke()
wenzelm@52494
   111
    }
wenzelm@52478
   112
wenzelm@52494
   113
wenzelm@52494
   114
  /* dismiss */
wenzelm@51452
   115
wenzelm@57612
   116
  private lazy val focus_delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
wenzelm@56341
   117
  {
wenzelm@56341
   118
    dismiss_unfocused()
wenzelm@56341
   119
  }
wenzelm@56341
   120
wenzelm@56341
   121
  def dismiss_unfocused()
wenzelm@56341
   122
  {
wenzelm@56341
   123
    stack.span(tip => !tip.pretty_text_area.isFocusOwner) match {
wenzelm@56341
   124
      case (Nil, _) =>
wenzelm@56341
   125
      case (unfocused, rest) =>
wenzelm@56341
   126
        deactivate()
wenzelm@56341
   127
        unfocused.foreach(_.hide_popup)
wenzelm@56341
   128
        stack = rest
wenzelm@56341
   129
    }
wenzelm@56341
   130
  }
wenzelm@56341
   131
wenzelm@52478
   132
  def dismiss(tip: Pretty_Tooltip)
wenzelm@52478
   133
  {
wenzelm@52494
   134
    deactivate()
wenzelm@52478
   135
    hierarchy(tip) match {
wenzelm@52478
   136
      case Some((old, _ :: rest)) =>
wenzelm@52498
   137
        rest match {
wenzelm@52498
   138
          case top :: _ => top.request_focus
wenzelm@56930
   139
          case Nil => JEdit_Lib.request_focus_view()
wenzelm@52498
   140
        }
wenzelm@54376
   141
        old.foreach(_.hide_popup)
wenzelm@54376
   142
        tip.hide_popup
wenzelm@54376
   143
        stack = rest
wenzelm@52478
   144
      case _ =>
wenzelm@52478
   145
    }
wenzelm@52478
   146
  }
wenzelm@52478
   147
wenzelm@56497
   148
  def dismiss_descendant(parent: JComponent): Unit =
wenzelm@56497
   149
    descendant(parent).foreach(dismiss(_))
wenzelm@56497
   150
wenzelm@52548
   151
  def dismissed_all(): Boolean =
wenzelm@52664
   152
  {
wenzelm@52664
   153
    deactivate()
wenzelm@52548
   154
    if (stack.isEmpty) false
wenzelm@52548
   155
    else {
wenzelm@56930
   156
      JEdit_Lib.request_focus_view()
wenzelm@52548
   157
      stack.foreach(_.hide_popup)
wenzelm@52548
   158
      stack = Nil
wenzelm@52548
   159
      true
wenzelm@52548
   160
    }
wenzelm@52664
   161
  }
wenzelm@51449
   162
}
wenzelm@51449
   163
wenzelm@51449
   164
wenzelm@52478
   165
class Pretty_Tooltip private(
wenzelm@52478
   166
  view: View,
wenzelm@53778
   167
  layered: JLayeredPane,
wenzelm@56497
   168
  val original_parent: JComponent,
wenzelm@53247
   169
  location: Point,
wenzelm@64621
   170
  rendering: JEdit_Rendering,
wenzelm@52496
   171
  private val results: Command.Results,
wenzelm@52496
   172
  private val info: Text.Info[XML.Body]) extends JPanel(new BorderLayout)
wenzelm@49702
   173
{
wenzelm@52478
   174
  tip =>
wenzelm@49705
   175
wenzelm@57612
   176
  GUI_Thread.require {}
wenzelm@49725
   177
wenzelm@49725
   178
wenzelm@49725
   179
  /* controls */
wenzelm@49725
   180
wenzelm@49727
   181
  private val close = new Label {
wenzelm@52478
   182
    icon = rendering.tooltip_close_icon
wenzelm@49727
   183
    tooltip = "Close tooltip window"
wenzelm@49727
   184
    listenTo(mouse.clicks)
wenzelm@52478
   185
    reactions += { case _: MouseClicked => Pretty_Tooltip.dismiss(tip) }
wenzelm@49727
   186
  }
wenzelm@49727
   187
wenzelm@49726
   188
  private val detach = new Label {
wenzelm@52478
   189
    icon = rendering.tooltip_detach_icon
wenzelm@49726
   190
    tooltip = "Detach tooltip window"
wenzelm@49726
   191
    listenTo(mouse.clicks)
wenzelm@49726
   192
    reactions += {
wenzelm@50501
   193
      case _: MouseClicked =>
wenzelm@52496
   194
        Info_Dockable(view, rendering.snapshot, results, info.info)
wenzelm@52478
   195
        Pretty_Tooltip.dismiss(tip)
wenzelm@49726
   196
    }
wenzelm@49726
   197
  }
wenzelm@49726
   198
wenzelm@52478
   199
  private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) {
wenzelm@52478
   200
    background = rendering.tooltip_color
wenzelm@49709
   201
  }
wenzelm@51452
   202
wenzelm@51452
   203
wenzelm@52478
   204
  /* text area */
wenzelm@52478
   205
wenzelm@52478
   206
  val pretty_text_area =
wenzelm@52478
   207
    new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) {
wenzelm@52478
   208
      override def get_background() = Some(rendering.tooltip_color)
wenzelm@52478
   209
    }
wenzelm@52478
   210
wenzelm@52478
   211
  pretty_text_area.addFocusListener(new FocusAdapter {
wenzelm@52491
   212
    override def focusGained(e: FocusEvent)
wenzelm@52491
   213
    {
wenzelm@52493
   214
      tip_border(true)
wenzelm@56341
   215
      Pretty_Tooltip.focus_delay.invoke()
wenzelm@52491
   216
    }
wenzelm@52478
   217
    override def focusLost(e: FocusEvent)
wenzelm@52478
   218
    {
wenzelm@56341
   219
      tip_border(false)
wenzelm@56341
   220
      Pretty_Tooltip.focus_delay.invoke()
wenzelm@52478
   221
    }
wenzelm@52478
   222
  })
wenzelm@51452
   223
wenzelm@55825
   224
  pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_popup_font_scale")))
wenzelm@52478
   225
wenzelm@52478
   226
wenzelm@52478
   227
  /* main content */
wenzelm@52478
   228
wenzelm@52493
   229
  def tip_border(has_focus: Boolean)
wenzelm@52491
   230
  {
wenzelm@52493
   231
    tip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY))
wenzelm@52491
   232
    tip.repaint()
wenzelm@52491
   233
  }
wenzelm@52493
   234
  tip_border(true)
wenzelm@52491
   235
wenzelm@52478
   236
  override def getFocusTraversalKeysEnabled = false
wenzelm@52478
   237
  tip.setBackground(rendering.tooltip_color)
wenzelm@52478
   238
  tip.add(controls.peer, BorderLayout.NORTH)
wenzelm@52478
   239
  tip.add(pretty_text_area)
wenzelm@52478
   240
wenzelm@52478
   241
wenzelm@52478
   242
  /* popup */
wenzelm@52478
   243
wenzelm@52478
   244
  private val popup =
wenzelm@51452
   245
  {
wenzelm@53247
   246
    val screen = JEdit_Lib.screen_location(layered, location)
wenzelm@53247
   247
    val size =
wenzelm@52492
   248
    {
wenzelm@64621
   249
      val bounds = JEdit_Rendering.popup_bounds
wenzelm@57849
   250
wenzelm@57849
   251
      val w_max = layered.getWidth min (screen.bounds.width * bounds).toInt
wenzelm@57849
   252
      val h_max = layered.getHeight min (screen.bounds.height * bounds).toInt
wenzelm@57849
   253
wenzelm@52492
   254
      val painter = pretty_text_area.getPainter
wenzelm@57849
   255
      val geometry = JEdit_Lib.window_geometry(tip, painter)
wenzelm@52492
   256
      val metric = JEdit_Lib.pretty_metric(painter)
wenzelm@57849
   257
wenzelm@57849
   258
      val margin =
wenzelm@57849
   259
        ((rendering.tooltip_margin * metric.average) min
wenzelm@57849
   260
          ((w_max - geometry.deco_width) / metric.unit).toInt) max 20
wenzelm@52492
   261
wenzelm@52496
   262
      val formatted = Pretty.formatted(info.info, margin, metric)
wenzelm@52492
   263
      val lines =
wenzelm@52492
   264
        XML.traverse_text(formatted)(0)(
wenzelm@52492
   265
          (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
wenzelm@52492
   266
wenzelm@58767
   267
      val h = painter.getLineHeight * (lines + 1) + geometry.deco_height
wenzelm@52492
   268
      val margin1 =
wenzelm@57849
   269
        if (h <= h_max)
wenzelm@52492
   270
          (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
wenzelm@52492
   271
        else margin
wenzelm@57849
   272
      val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
wenzelm@53184
   273
wenzelm@57849
   274
      new Dimension(w min w_max, h min h_max)
wenzelm@52492
   275
    }
wenzelm@53247
   276
    new Popup(layered, tip, screen.relative(layered, size), size)
wenzelm@51452
   277
  }
wenzelm@52478
   278
wenzelm@52484
   279
  private def show_popup
wenzelm@52484
   280
  {
wenzelm@52484
   281
    popup.show
wenzelm@52484
   282
    pretty_text_area.requestFocus
wenzelm@52496
   283
    pretty_text_area.update(rendering.snapshot, results, info.info)
wenzelm@52484
   284
  }
wenzelm@52478
   285
wenzelm@52478
   286
  private def hide_popup: Unit = popup.hide
wenzelm@52498
   287
wenzelm@52498
   288
  private def request_focus: Unit = pretty_text_area.requestFocus
wenzelm@49702
   289
}
wenzelm@49702
   290