src/Tools/jEdit/src/jedit/output_dockable.scala

--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Jan 11 18:28:31 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Jan 11 20:51:58 2010 +0100
@@ -38,9 +38,7 @@
           Swing_Thread.now { Document_Model(view.getBuffer) } match {
             case None =>
             case Some(model) =>
-              val body =
-                if (cmd == null) Nil  // FIXME ??
-                else model.recent_document.current_state(cmd).results
+              val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
               html_panel.render(body)
           }