src/Tools/jEdit/src/output_dockable.scala

--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Sep 03 09:15:58 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Sep 03 10:17:17 2012 +0200
@@ -107,9 +107,9 @@
                     case _ => true
                   }).toList
               html_panel.render(filtered_results)
-            case _ =>
+            case _ => html_panel.render(Nil)
           }
-        case None =>
+        case None => html_panel.render(Nil)
       }
     }
   }