--- 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