retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
authorwenzelm
Sat Mar 23 19:39:31 2013 +0100 (2013-03-23 ago)
changeset 51496cb677987b7e3
parent 51495 5944b20c41bf
child 51497 7e8968c9a549
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
src/Pure/PIDE/command.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Mar 23 16:46:09 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Mar 23 19:39:31 2013 +0100
     1.3 @@ -21,7 +21,9 @@
     1.4  
     1.5    object Results
     1.6    {
     1.7 +    type Entry = (Long, XML.Tree)
     1.8      val empty = new Results(SortedMap.empty)
     1.9 +    def make(es: Iterable[Results.Entry]): Results = (empty /: es.iterator)(_ + _)
    1.10      def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
    1.11    }
    1.12  
    1.13 @@ -29,9 +31,9 @@
    1.14    {
    1.15      def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
    1.16      def get(serial: Long): Option[XML.Tree] = rep.get(serial)
    1.17 -    def entries: Iterator[(Long, XML.Tree)] = rep.iterator
    1.18 +    def entries: Iterator[Results.Entry] = rep.iterator
    1.19  
    1.20 -    def + (entry: (Long, XML.Tree)): Results =
    1.21 +    def + (entry: Results.Entry): Results =
    1.22        if (defined(entry._1)) this
    1.23        else new Results(rep + entry)
    1.24  
     2.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Sat Mar 23 16:46:09 2013 +0100
     2.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sat Mar 23 19:39:31 2013 +0100
     2.3 @@ -65,7 +65,8 @@
     2.4            override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
     2.5            {
     2.6              val rendering = Rendering(snapshot, PIDE.options.value)
     2.7 -            Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
     2.8 +            Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty,
     2.9 +              Text.Range(-1), body)
    2.10              null
    2.11            }
    2.12          }
     3.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 23 16:46:09 2013 +0100
     3.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 23 19:39:31 2013 +0100
     3.3 @@ -39,6 +39,7 @@
     3.4      rendering: Rendering,
     3.5      mouse_x: Int, mouse_y: Int,
     3.6      results: Command.Results,
     3.7 +    range: Text.Range,
     3.8      body: XML.Body): Pretty_Tooltip =
     3.9    {
    3.10      Swing_Thread.require()
    3.11 @@ -63,7 +64,7 @@
    3.12            others.foreach(_.dispose)
    3.13            window
    3.14        }
    3.15 -    window.init(rendering, parent, mouse_x, mouse_y, results, body)
    3.16 +    window.init(rendering, parent, mouse_x, mouse_y, results, range, body)
    3.17      window
    3.18    }
    3.19  
    3.20 @@ -104,6 +105,7 @@
    3.21    private var current_rendering: Rendering =
    3.22      Rendering(Document.State.init.snapshot(), PIDE.options.value)
    3.23    private var current_results = Command.Results.empty
    3.24 +  private var current_range = Text.Range(-1)
    3.25    private var current_body: XML.Body = Nil
    3.26  
    3.27  
    3.28 @@ -168,60 +170,64 @@
    3.29      parent: JComponent,
    3.30      mouse_x: Int, mouse_y: Int,
    3.31      results: Command.Results,
    3.32 +    range: Text.Range,
    3.33      body: XML.Body)
    3.34    {
    3.35 -    current_rendering = rendering
    3.36 -    current_results = results
    3.37 -    current_body = body
    3.38 +    if (!(results == current_results && range == current_range && body == current_body)) {
    3.39 +      current_rendering = rendering
    3.40 +      current_results = results
    3.41 +      current_range = range
    3.42 +      current_body = body
    3.43  
    3.44 -    pretty_text_area.resize(Rendering.font_family(),
    3.45 -      Rendering.font_size("jedit_tooltip_font_scale").round)
    3.46 -    pretty_text_area.update(rendering.snapshot, results, body)
    3.47 +      pretty_text_area.resize(Rendering.font_family(),
    3.48 +        Rendering.font_size("jedit_tooltip_font_scale").round)
    3.49 +      pretty_text_area.update(rendering.snapshot, results, body)
    3.50  
    3.51 -    content_panel.setBackground(rendering.tooltip_color)
    3.52 -    controls.background = rendering.tooltip_color
    3.53 +      content_panel.setBackground(rendering.tooltip_color)
    3.54 +      controls.background = rendering.tooltip_color
    3.55  
    3.56  
    3.57 -    /* window geometry */
    3.58 +      /* window geometry */
    3.59 +
    3.60 +      val screen_point = new Point(mouse_x, mouse_y)
    3.61 +      SwingUtilities.convertPointToScreen(screen_point, parent)
    3.62 +      val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
    3.63  
    3.64 -    val screen_point = new Point(mouse_x, mouse_y)
    3.65 -    SwingUtilities.convertPointToScreen(screen_point, parent)
    3.66 -    val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
    3.67 +      {
    3.68 +        val painter = pretty_text_area.getPainter
    3.69 +        val metric = JEdit_Lib.pretty_metric(painter)
    3.70 +        val margin = rendering.tooltip_margin * metric.average
    3.71 +        val lines =
    3.72 +          XML.traverse_text(Pretty.formatted(body, margin, metric))(0)(
    3.73 +            (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
    3.74  
    3.75 -    {
    3.76 -      val painter = pretty_text_area.getPainter
    3.77 -      val metric = JEdit_Lib.pretty_metric(painter)
    3.78 -      val margin = rendering.tooltip_margin * metric.average
    3.79 -      val lines =
    3.80 -        XML.traverse_text(Pretty.formatted(body, margin, metric))(0)(
    3.81 -          (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
    3.82 +        if (window.getWidth == 0) {
    3.83 +          window.setSize(new Dimension(100, 100))
    3.84 +          window.setPreferredSize(new Dimension(100, 100))
    3.85 +        }
    3.86 +        window.pack
    3.87 +        window.revalidate
    3.88 +
    3.89 +        val deco_width = window.getWidth - painter.getWidth
    3.90 +        val deco_height = window.getHeight - painter.getHeight
    3.91  
    3.92 -      if (window.getWidth == 0) {
    3.93 -        window.setSize(new Dimension(100, 100))
    3.94 -        window.setPreferredSize(new Dimension(100, 100))
    3.95 +        val bounds = rendering.tooltip_bounds
    3.96 +        val w =
    3.97 +          ((metric.unit * (margin + metric.average)).round.toInt + deco_width) min
    3.98 +          (screen_bounds.width * bounds).toInt
    3.99 +        val h =
   3.100 +          (painter.getFontMetrics.getHeight * (lines + 1) + deco_height) min
   3.101 +          (screen_bounds.height * bounds).toInt
   3.102 +
   3.103 +        window.setSize(new Dimension(w, h))
   3.104 +        window.setPreferredSize(new Dimension(w, h))
   3.105 +        window.pack
   3.106 +        window.revalidate
   3.107 +
   3.108 +        val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
   3.109 +        val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
   3.110 +        window.setLocation(x, y)
   3.111        }
   3.112 -      window.pack
   3.113 -      window.revalidate
   3.114 -
   3.115 -      val deco_width = window.getWidth - painter.getWidth
   3.116 -      val deco_height = window.getHeight - painter.getHeight
   3.117 -
   3.118 -      val bounds = rendering.tooltip_bounds
   3.119 -      val w =
   3.120 -        ((metric.unit * (margin + metric.average)).round.toInt + deco_width) min
   3.121 -        (screen_bounds.width * bounds).toInt
   3.122 -      val h =
   3.123 -        (painter.getFontMetrics.getHeight * (lines + 1) + deco_height) min
   3.124 -        (screen_bounds.height * bounds).toInt
   3.125 -
   3.126 -      window.setSize(new Dimension(w, h))
   3.127 -      window.setPreferredSize(new Dimension(w, h))
   3.128 -      window.pack
   3.129 -      window.revalidate
   3.130 -
   3.131 -      val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
   3.132 -      val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
   3.133 -      window.setLocation(x, y)
   3.134      }
   3.135  
   3.136      window.setVisible(true)
     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 23 16:46:09 2013 +0100
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 23 19:39:31 2013 +0100
     4.3 @@ -275,22 +275,30 @@
     4.4      (Command.Results.empty /: results)(_ ++ _)
     4.5    }
     4.6  
     4.7 -  def tooltip_message(range: Text.Range): XML.Body =
     4.8 +  def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
     4.9    {
    4.10 -    val msgs =
    4.11 -      Command.Results.merge(
    4.12 -        snapshot.cumulate_markup[Command.Results](range, Command.Results.empty,
    4.13 -          Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
    4.14 -          {
    4.15 -            case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
    4.16 -            if name == Markup.WRITELN ||
    4.17 -                name == Markup.WARNING ||
    4.18 -                name == Markup.ERROR =>
    4.19 -              msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
    4.20 -            case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
    4.21 -            if !body.isEmpty => msgs + (Document.new_id() -> msg)
    4.22 -          }).map(_.info))
    4.23 -    Pretty.separate(msgs.entries.map(_._2).toList)
    4.24 +    val results =
    4.25 +      snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](range, Nil,
    4.26 +        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
    4.27 +        {
    4.28 +          case (msgs, Text.Info(info_range,
    4.29 +            XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
    4.30 +          if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
    4.31 +            val entry: Command.Results.Entry =
    4.32 +              (serial -> XML.Elem(Markup(Markup.message(name), props), body))
    4.33 +            Text.Info(snapshot.convert(info_range), entry) :: msgs
    4.34 +
    4.35 +          case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
    4.36 +          if !body.isEmpty =>
    4.37 +            val entry: Command.Results.Entry = (Document.new_id(), msg)
    4.38 +            Text.Info(snapshot.convert(info_range), entry) :: msgs
    4.39 +        }).toList.flatMap(_.info)
    4.40 +    if (results.isEmpty) None
    4.41 +    else {
    4.42 +      val r = Text.Range(results.head.range.start, results.last.range.stop)
    4.43 +      val msgs = Command.Results.make(results.map(_.info))
    4.44 +      Some(Text.Info(r, Pretty.separate(msgs.entries.map(_._2).toList)))
    4.45 +    }
    4.46    }
    4.47  
    4.48  
    4.49 @@ -317,12 +325,15 @@
    4.50    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    4.51      Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
    4.52  
    4.53 -  def tooltip(range: Text.Range): XML.Body =
    4.54 +  def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
    4.55    {
    4.56 -    def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r: Text.Range, p: (Boolean, XML.Tree)) =
    4.57 +    def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r0: Text.Range, p: (Boolean, XML.Tree)) =
    4.58 +    {
    4.59 +      val r = snapshot.convert(r0)
    4.60        if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
    4.61 +    }
    4.62  
    4.63 -    val tips =
    4.64 +    val results =
    4.65        snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
    4.66          range, Text.Info(range, Nil), Some(tooltip_elements), _ =>
    4.67          {
    4.68 @@ -340,11 +351,15 @@
    4.69              add(prev, r, (false, pretty_typing("ML:", body)))
    4.70            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
    4.71            if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
    4.72 -        }).toList.flatMap(_.info.info)
    4.73 +        }).toList.map(_.info)
    4.74  
    4.75 -    val all_tips =
    4.76 -      (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
    4.77 -    Library.separate(Pretty.FBreak, all_tips.toList)
    4.78 +    results.flatMap(_.info) match {
    4.79 +      case Nil => None
    4.80 +      case tips =>
    4.81 +        val r = Text.Range(results.head.range.start, results.last.range.stop)
    4.82 +        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
    4.83 +        Some(Text.Info(r, Library.separate(Pretty.FBreak, all_tips)))
    4.84 +    }
    4.85    }
    4.86  
    4.87    val tooltip_margin: Int = options.int("jedit_tooltip_margin")
     5.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 23 16:46:09 2013 +0100
     5.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 23 19:39:31 2013 +0100
     5.3 @@ -215,14 +215,16 @@
     5.4              JEdit_Lib.pixel_range(text_area, x, y) match {
     5.5                case None =>
     5.6                case Some(range) =>
     5.7 -                val tip =
     5.8 +                val result =
     5.9                    if (control) rendering.tooltip(range)
    5.10                    else rendering.tooltip_message(range)
    5.11 -                if (!tip.isEmpty) {
    5.12 -                  val painter = text_area.getPainter
    5.13 -                  val y1 = y + painter.getFontMetrics.getHeight / 2
    5.14 -                  val results = rendering.command_results(range)
    5.15 -                  Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
    5.16 +                result match {
    5.17 +                  case None =>
    5.18 +                  case Some(tip) =>
    5.19 +                    val painter = text_area.getPainter
    5.20 +                    val y1 = y + painter.getFontMetrics.getHeight / 2
    5.21 +                    val results = rendering.command_results(range)
    5.22 +                    Pretty_Tooltip(view, painter, rendering, x, y1, results, tip.range, tip.info)
    5.23                  }
    5.24              }
    5.25            }