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