# HG changeset patch # User wenzelm # Date 1364063971 -3600 # Node ID cb677987b7e3deb8a2e5d87e9e7da610eed62734 # Parent 5944b20c41bfb64915abe79ce3ede642189f83a8 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content; diff -r 5944b20c41bf -r cb677987b7e3 src/Pure/PIDE/command.scala --- 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) diff -r 5944b20c41bf -r cb677987b7e3 src/Tools/jEdit/src/graphview_dockable.scala --- 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 } } diff -r 5944b20c41bf -r cb677987b7e3 src/Tools/jEdit/src/pretty_tooltip.scala --- 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) diff -r 5944b20c41bf -r cb677987b7e3 src/Tools/jEdit/src/rendering.scala --- 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") diff -r 5944b20c41bf -r cb677987b7e3 src/Tools/jEdit/src/rich_text_area.scala --- 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) } } }