# HG changeset patch
# User wenzelm
# Date 1483353735 -3600
# Node ID 155bf86321041d2006ad8fbb1f93ee624276ba79
# Parent  54afac94f52b0013b17ab21c08d90d7929d67871
clarified multiple tooltips;

diff -r 54afac94f52b -r 155bf8632104 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Jan 02 11:26:26 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Jan 02 11:42:15 2017 +0100
@@ -73,7 +73,7 @@
   def tooltip_margin: Int
   def timing_threshold: Double
 
-  def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
+  def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
   {
     def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
       r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
@@ -159,7 +159,7 @@
       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.fbrk, all_tips)))
+        Some(Text.Info(r, all_tips))
     }
   }
 }
diff -r 54afac94f52b -r 155bf8632104 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Jan 02 11:26:26 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Mon Jan 02 11:42:15 2017 +0100
@@ -280,12 +280,13 @@
     val result =
       for {
         (rendering, offset) <- rendering_offset(node_pos)
-        info <- rendering.tooltip(Text.Range(offset, offset + 1))
+        info <- rendering.tooltips(Text.Range(offset, offset + 1))
       } yield {
         val doc = rendering.model.doc
         val range = doc.range(info.range)
-        val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
-        (range, List(s))
+        val contents =
+          info.info.map(tree => Pretty.string_of(List(tree), margin = rendering.tooltip_margin))
+        (range, contents)
       }
     channel.write(Protocol.Hover.reply(id, result))
   }
diff -r 54afac94f52b -r 155bf8632104 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Jan 02 11:26:26 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Jan 02 11:42:15 2017 +0100
@@ -525,6 +525,10 @@
   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)) })
+
   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"))