src/Tools/jEdit/src/graphview_dockable.scala

--- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Dec 13 19:53:55 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Fri Dec 14 12:09:08 2012 +0100
@@ -65,7 +65,7 @@
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
           {
             val rendering = Rendering(snapshot, PIDE.options.value)
-            new Pretty_Tooltip(view, parent, rendering, x, y, Command.empty_results, body)
+            new Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
             null
           }
         }