retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
--- a/src/Pure/PIDE/command.scala Sat Mar 23 16:46:09 2013 +0100
+++ b/src/Pure/PIDE/command.scala Sat Mar 23 19:39:31 2013 +0100
@@ -21,7 +21,9 @@
object Results
{
+ type Entry = (Long, XML.Tree)
val empty = new Results(SortedMap.empty)
+ def make(es: Iterable[Results.Entry]): Results = (empty /: es.iterator)(_ + _)
def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
}
@@ -29,9 +31,9 @@
{
def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
def get(serial: Long): Option[XML.Tree] = rep.get(serial)
- def entries: Iterator[(Long, XML.Tree)] = rep.iterator
+ def entries: Iterator[Results.Entry] = rep.iterator
- def + (entry: (Long, XML.Tree)): Results =
+ def + (entry: Results.Entry): Results =
if (defined(entry._1)) this
else new Results(rep + entry)
--- a/src/Tools/jEdit/src/graphview_dockable.scala Sat Mar 23 16:46:09 2013 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sat Mar 23 19:39:31 2013 +0100
@@ -65,7 +65,8 @@
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
{
val rendering = Rendering(snapshot, PIDE.options.value)
- Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
+ Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty,
+ Text.Range(-1), body)
null
}
}
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 23 16:46:09 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 23 19:39:31 2013 +0100
@@ -39,6 +39,7 @@
rendering: Rendering,
mouse_x: Int, mouse_y: Int,
results: Command.Results,
+ range: Text.Range,
body: XML.Body): Pretty_Tooltip =
{
Swing_Thread.require()
@@ -63,7 +64,7 @@
others.foreach(_.dispose)
window
}
- window.init(rendering, parent, mouse_x, mouse_y, results, body)
+ window.init(rendering, parent, mouse_x, mouse_y, results, range, body)
window
}
@@ -104,6 +105,7 @@
private var current_rendering: Rendering =
Rendering(Document.State.init.snapshot(), PIDE.options.value)
private var current_results = Command.Results.empty
+ private var current_range = Text.Range(-1)
private var current_body: XML.Body = Nil
@@ -168,60 +170,64 @@
parent: JComponent,
mouse_x: Int, mouse_y: Int,
results: Command.Results,
+ range: Text.Range,
body: XML.Body)
{
- current_rendering = rendering
- current_results = results
- current_body = body
+ if (!(results == current_results && range == current_range && body == current_body)) {
+ current_rendering = rendering
+ current_results = results
+ current_range = range
+ current_body = body
- pretty_text_area.resize(Rendering.font_family(),
- Rendering.font_size("jedit_tooltip_font_scale").round)
- pretty_text_area.update(rendering.snapshot, results, body)
+ pretty_text_area.resize(Rendering.font_family(),
+ Rendering.font_size("jedit_tooltip_font_scale").round)
+ pretty_text_area.update(rendering.snapshot, results, body)
- content_panel.setBackground(rendering.tooltip_color)
- controls.background = rendering.tooltip_color
+ content_panel.setBackground(rendering.tooltip_color)
+ controls.background = rendering.tooltip_color
- /* window geometry */
+ /* window geometry */
+
+ val screen_point = new Point(mouse_x, mouse_y)
+ SwingUtilities.convertPointToScreen(screen_point, parent)
+ val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
- val screen_point = new Point(mouse_x, mouse_y)
- SwingUtilities.convertPointToScreen(screen_point, parent)
- val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
+ {
+ val painter = pretty_text_area.getPainter
+ val metric = JEdit_Lib.pretty_metric(painter)
+ val margin = rendering.tooltip_margin * metric.average
+ val lines =
+ XML.traverse_text(Pretty.formatted(body, margin, metric))(0)(
+ (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
- {
- val painter = pretty_text_area.getPainter
- val metric = JEdit_Lib.pretty_metric(painter)
- val margin = rendering.tooltip_margin * metric.average
- val lines =
- XML.traverse_text(Pretty.formatted(body, margin, metric))(0)(
- (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
+ if (window.getWidth == 0) {
+ window.setSize(new Dimension(100, 100))
+ window.setPreferredSize(new Dimension(100, 100))
+ }
+ window.pack
+ window.revalidate
+
+ val deco_width = window.getWidth - painter.getWidth
+ val deco_height = window.getHeight - painter.getHeight
- if (window.getWidth == 0) {
- window.setSize(new Dimension(100, 100))
- window.setPreferredSize(new Dimension(100, 100))
+ val bounds = rendering.tooltip_bounds
+ val w =
+ ((metric.unit * (margin + metric.average)).round.toInt + deco_width) min
+ (screen_bounds.width * bounds).toInt
+ val h =
+ (painter.getFontMetrics.getHeight * (lines + 1) + deco_height) min
+ (screen_bounds.height * bounds).toInt
+
+ window.setSize(new Dimension(w, h))
+ window.setPreferredSize(new Dimension(w, h))
+ window.pack
+ window.revalidate
+
+ val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
+ val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
+ window.setLocation(x, y)
}
- window.pack
- window.revalidate
-
- val deco_width = window.getWidth - painter.getWidth
- val deco_height = window.getHeight - painter.getHeight
-
- val bounds = rendering.tooltip_bounds
- val w =
- ((metric.unit * (margin + metric.average)).round.toInt + deco_width) min
- (screen_bounds.width * bounds).toInt
- val h =
- (painter.getFontMetrics.getHeight * (lines + 1) + deco_height) min
- (screen_bounds.height * bounds).toInt
-
- window.setSize(new Dimension(w, h))
- window.setPreferredSize(new Dimension(w, h))
- window.pack
- window.revalidate
-
- val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
- val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
- window.setLocation(x, y)
}
window.setVisible(true)
--- a/src/Tools/jEdit/src/rendering.scala Sat Mar 23 16:46:09 2013 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sat Mar 23 19:39:31 2013 +0100
@@ -275,22 +275,30 @@
(Command.Results.empty /: results)(_ ++ _)
}
- def tooltip_message(range: Text.Range): XML.Body =
+ def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
{
- val msgs =
- Command.Results.merge(
- snapshot.cumulate_markup[Command.Results](range, Command.Results.empty,
- Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
- {
- case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
- if name == Markup.WRITELN ||
- name == Markup.WARNING ||
- name == Markup.ERROR =>
- msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
- case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
- if !body.isEmpty => msgs + (Document.new_id() -> msg)
- }).map(_.info))
- Pretty.separate(msgs.entries.map(_._2).toList)
+ val results =
+ snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](range, Nil,
+ Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
+ {
+ case (msgs, Text.Info(info_range,
+ XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
+ if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
+ val entry: Command.Results.Entry =
+ (serial -> XML.Elem(Markup(Markup.message(name), props), body))
+ Text.Info(snapshot.convert(info_range), entry) :: msgs
+
+ case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
+ if !body.isEmpty =>
+ val entry: Command.Results.Entry = (Document.new_id(), msg)
+ Text.Info(snapshot.convert(info_range), entry) :: msgs
+ }).toList.flatMap(_.info)
+ if (results.isEmpty) None
+ else {
+ val r = Text.Range(results.head.range.start, results.last.range.stop)
+ val msgs = Command.Results.make(results.map(_.info))
+ Some(Text.Info(r, Pretty.separate(msgs.entries.map(_._2).toList)))
+ }
}
@@ -317,12 +325,15 @@
private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
- def tooltip(range: Text.Range): XML.Body =
+ def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
{
- def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r: Text.Range, p: (Boolean, XML.Tree)) =
+ def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r0: Text.Range, p: (Boolean, XML.Tree)) =
+ {
+ val r = snapshot.convert(r0)
if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
+ }
- val tips =
+ val results =
snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
range, Text.Info(range, Nil), Some(tooltip_elements), _ =>
{
@@ -340,11 +351,15 @@
add(prev, r, (false, pretty_typing("ML:", body)))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
- }).toList.flatMap(_.info.info)
+ }).toList.map(_.info)
- val all_tips =
- (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
- Library.separate(Pretty.FBreak, all_tips.toList)
+ results.flatMap(_.info) match {
+ case Nil => None
+ case tips =>
+ val r = Text.Range(results.head.range.start, results.last.range.stop)
+ val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
+ Some(Text.Info(r, Library.separate(Pretty.FBreak, all_tips)))
+ }
}
val tooltip_margin: Int = options.int("jedit_tooltip_margin")
--- a/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 23 16:46:09 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 23 19:39:31 2013 +0100
@@ -215,14 +215,16 @@
JEdit_Lib.pixel_range(text_area, x, y) match {
case None =>
case Some(range) =>
- val tip =
+ val result =
if (control) rendering.tooltip(range)
else rendering.tooltip_message(range)
- if (!tip.isEmpty) {
- val painter = text_area.getPainter
- val y1 = y + painter.getFontMetrics.getHeight / 2
- val results = rendering.command_results(range)
- Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
+ result match {
+ case None =>
+ case Some(tip) =>
+ val painter = text_area.getPainter
+ val y1 = y + painter.getFontMetrics.getHeight / 2
+ val results = rendering.command_results(range)
+ Pretty_Tooltip(view, painter, rendering, x, y1, results, tip.range, tip.info)
}
}
}