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