# HG changeset patch
# User wenzelm
# Date 1346660237 -7200
# Node ID c1ca931b36476ebf67be3e000df940f1c2f4b10d
# Parent  f00fee6d21d4a5c1850506d884da8fc1507567ef
actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);

diff -r f00fee6d21d4 -r c1ca931b3647 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)
       }
     }
   }