more general tooltips, with uniform info range handling;

--- 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, _ =>

--- 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)

--- 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"))