# HG changeset patch # User wenzelm # Date 1488815272 -3600 # Node ID 06a7c2d316cf0857fe2f65882f06703677a1925b # Parent 93a1e3b1ede0762825601cc96a47aceed72c76c2 more general tooltips, with uniform info range handling; diff -r 93a1e3b1ede0 -r 06a7c2d316cf src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Mon Mar 06 11:48:06 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Mon Mar 06 16:47:52 2017 +0100 @@ -126,12 +126,16 @@ Markup.TFREE -> "free type variable", Markup.TVAR -> "schematic type variable") - private val tooltip_elements = + val tooltip_elements = Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet) + val tooltip_message_elements = + Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR, + Markup.BAD) + private def pretty_typing(kind: String, body: XML.Body): XML.Tree = Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body) @@ -168,93 +172,108 @@ def timing_threshold: Double - def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] = + private sealed case class Tooltip_Info( + range: Text.Range, + timing: Timing = Timing.zero, + messages: List[Command.Results.Entry] = Nil, + rev_infos: List[(Boolean, XML.Tree)] = Nil) { - def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])], - r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] = + def + (t: Timing): Tooltip_Info = copy(timing = timing + t) + def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info = + { + val r = snapshot.convert(r0) + if (range == r) copy(messages = (serial -> tree) :: messages) + else copy(range = r, messages = List(serial -> tree)) + } + def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info = { val r = snapshot.convert(r0) - val (t, info) = prev.info - if (prev.range == r) - Text.Info(r, (t, info :+ p)) - else Text.Info(r, (t, Vector(p))) + if (range == r) copy(rev_infos = (important -> tree) :: rev_infos) + else copy (range = r, rev_infos = List(important -> tree)) } + def infos(important: Boolean): List[XML.Tree] = + rev_infos.filter(p => p._1 == important).reverse.map(_._2) + } + def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] = + { val results = - snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]]( - range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ => + snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, _ => { - case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) => - Some(Text.Info(r, (t1 + t2, info))) + case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t) - case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) + case (info, Text.Info(r0, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) + if Rendering.tooltip_message_elements(name) && body.nonEmpty => + Some(info + (r0, serial, XML.Elem(Markup(Markup.message(name), props), body))) + + case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _))) if kind != "" && kind != Markup.ML_DEF => val kind1 = Word.implode(Word.explode('_', kind)) val txt1 = if (name == "") kind1 else if (kind1 == "") quote(name) else kind1 + " " + quote(name) - val t = prev.info._1 val txt2 = - if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold) - "\n" + t.message + if (kind == Markup.COMMAND && info.timing.elapsed.seconds >= timing_threshold) + "\n" + info.timing.message else "" - Some(add(prev, r, (true, XML.Text(txt1 + txt2)))) + Some(info + (r0, true, XML.Text(txt1 + txt2))) - case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) => + case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) => val file = resources.append_file(snapshot.node_name.master_dir, name) val text = if (name == file) "file " + quote(file) else "path " + quote(name) + "\nfile " + quote(file) - Some(add(prev, r, (true, XML.Text(text)))) + Some(info + (r0, true, XML.Text(text))) - case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) => + case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) => val text = "doc " + quote(name) - Some(add(prev, r, (true, XML.Text(text)))) + Some(info + (r0, true, XML.Text(text))) - case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) => - Some(add(prev, r, (true, XML.Text("URL " + quote(name))))) + case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) => + Some(info + (r0, true, XML.Text("URL " + quote(name)))) - case (prev, Text.Info(r, XML.Elem(Markup(name, _), body))) + case (info, Text.Info(r0, XML.Elem(Markup(name, _), body))) if name == Markup.SORTING || name == Markup.TYPING => - Some(add(prev, r, (true, Rendering.pretty_typing("::", body)))) + Some(info + (r0, true, Rendering.pretty_typing("::", body))) - case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) => - Some(add(prev, r, (true, Pretty.block(0, body)))) + case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) => + Some(info + (r0, true, Pretty.block(0, body))) - case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => - Some(add(prev, r, (false, Rendering.pretty_typing("ML:", body)))) + case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => + Some(info + (r0, false, Rendering.pretty_typing("ML:", body))) - case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) => + case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) => val text = if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)" else "breakpoint (disabled)" - Some(add(prev, r, (true, XML.Text(text)))) + Some(info + (r0, true, XML.Text(text))) - case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) => + case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) => val lang = Word.implode(Word.explode('_', language)) - Some(add(prev, r, (true, XML.Text("language: " + lang)))) + Some(info + (r0, true, XML.Text("language: " + lang))) - case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) => + case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) => val descr = if (kind == "") "expression" else "expression: " + kind - Some(add(prev, r, (true, XML.Text(descr)))) + Some(info + (r0, true, XML.Text(descr))) - case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) => - Some(add(prev, r, (true, XML.Text("Markdown: paragraph")))) - case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) => - Some(add(prev, r, (true, XML.Text("Markdown: " + kind)))) + case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) => + Some(info + (r0, true, XML.Text("Markdown: paragraph"))) + case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) => + Some(info + (r0, true, XML.Text("Markdown: " + kind))) - case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) => - Rendering.tooltip_descriptions.get(name). - map(descr => add(prev, r, (true, XML.Text(descr)))) + case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) => + Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc))) }).map(_.info) - results.map(_.info).flatMap(res => res._2.toList) 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, all_tips)) + if (results.isEmpty) None + else { + val r = Text.Range(results.head.range.start, results.last.range.stop) + val all_tips = + Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList ::: + results.flatMap(res => res.infos(true)) ::: + results.flatMap(res => res.infos(false)).lastOption.toList + if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips)) } } @@ -380,8 +399,8 @@ /* message underline color */ - def message_underline_color( - elements: Markup.Elements, range: Text.Range): List[Text.Info[Rendering.Color.Value]] = + def message_underline_color(elements: Markup.Elements, range: Text.Range) + : List[Text.Info[Rendering.Color.Value]] = { val results = snapshot.cumulate[Int](range, 0, elements, _ => diff -r 93a1e3b1ede0 -r 06a7c2d316cf src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Mon Mar 06 11:48:06 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Mon Mar 06 16:47:52 2017 +0100 @@ -300,7 +300,7 @@ val result = for { (rendering, offset) <- rendering_offset(node_pos) - info <- rendering.tooltips(Text.Range(offset, offset + 1)) + info <- rendering.tooltips(Rendering.tooltip_elements, Text.Range(offset, offset + 1)) } yield { val doc = rendering.model.content.doc val range = doc.range(info.range) diff -r 93a1e3b1ede0 -r 06a7c2d316cf src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Mon Mar 06 11:48:06 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Mar 06 16:47:52 2017 +0100 @@ -135,10 +135,6 @@ Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION, Markup.CITATION, Markup.URL) - private val tooltip_message_elements = - Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR, - Markup.BAD) - private val gutter_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) @@ -394,40 +390,18 @@ { case _ => Some(command_states) }).flatMap(_.info)) - /* tooltip messages */ - - def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] = - { - val results = - snapshot.cumulate[List[Text.Info[Command.Results.Entry]]]( - range, Nil, JEdit_Rendering.tooltip_message_elements, _ => - { - case (msgs, Text.Info(info_range, - XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) - if body.nonEmpty => - val entry: Command.Results.Entry = - serial -> XML.Elem(Markup(Markup.message(name), props), body) - Some(Text.Info(snapshot.convert(info_range), entry) :: msgs) - - case _ => None - }).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.iterator.map(_._2).toList))) - } - } - - /* tooltips */ def tooltip_margin: Int = options.int("jedit_tooltip_margin") def timing_threshold: Double = options.real("jedit_timing_threshold") def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] = - tooltips(range).map({ case Text.Info(r, all_tips) => - Text.Info(r, Library.separate(Pretty.fbrk, all_tips)) }) + for (Text.Info(r, tips) <- tooltips(Rendering.tooltip_elements, range)) + yield Text.Info(r, Library.separate(Pretty.fbrk, tips)) + + def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] = + for (Text.Info(r, tips) <- tooltips(Rendering.tooltip_message_elements, range)) + yield Text.Info(r, Library.separate(Pretty.fbrk, tips)) lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon")) lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))