actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);
authorwenzelm
Mon, 03 Sep 2012 10:17:17 +0200
changeset 49071 c1ca931b3647
parent 49070 f00fee6d21d4
child 49072 747835eb2782
actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);
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)
       }
     }
   }