src/Tools/jEdit/src/jedit/output_dockable.scala
changeset 38152 eab0d1c2e46e
parent 38151 2837c952ca31
child 38223 2a368e8e0a80
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Aug 05 18:00:37 2010 +0200
@@ -65,9 +65,9 @@
         case Some(doc_view) =>
           current_command match {
             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
-              val document = doc_view.model.snapshot().document
+              val snapshot = doc_view.model.snapshot()
               val filtered_results =
-                document.current_state(cmd).results filter {
+                snapshot.document.current_state(cmd).results filter {
                   case XML.Elem(Markup.TRACING, _, _) => show_tracing
                   case XML.Elem(Markup.DEBUG, _, _) => show_debug
                   case _ => true