src/Tools/jEdit/src/pretty_tooltip.scala

 
 class Pretty_Tooltip(
   view: View,
   parent: JComponent,
   rendering: Rendering,
-  mouse_x: Int, mouse_y: Int, body: XML.Body)
+  mouse_x: Int, mouse_y: Int,
+  results: Command.Results,
+  body: XML.Body)
   extends JWindow(JEdit_Lib.parent_window(parent) getOrElse view)
 {
   window =>
 
   Swing_Thread.require()

 
   val pretty_text_area = new Pretty_Text_Area(view)
   pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
   pretty_text_area.resize(Rendering.font_family(),
     Rendering.font_size("jedit_tooltip_font_scale").round)
-  pretty_text_area.update(rendering.snapshot, body)
+  pretty_text_area.update(rendering.snapshot, results, body)
 
   pretty_text_area.registerKeyboardAction(action_listener, "close_all",
     KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
 
   window.add(pretty_text_area)

   private val detach = new Label {
     icon = Rendering.tooltip_detach_icon
     tooltip = "Detach tooltip window"
     listenTo(mouse.clicks)
     reactions += {
-      case _: MouseClicked => Info_Dockable(view, rendering.snapshot, body); window.dispose()
+      case _: MouseClicked =>
+        Info_Dockable(view, rendering.snapshot, results, body)
+        window.dispose()
     }
   }
 
   private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) {
     background = rendering.tooltip_color