src/Tools/jEdit/src/jedit/output_dockable.scala
changeset 38872 26c505765024
parent 38360 53224a4d2f0e
child 39513 fce2202892c4
     1.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Aug 30 11:35:17 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Aug 30 13:01:32 2010 +0200
     1.3 @@ -67,12 +67,12 @@
     1.4              case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
     1.5                val snapshot = doc_view.model.snapshot()
     1.6                val filtered_results =
     1.7 -                snapshot.state(cmd).results filter {
     1.8 +                snapshot.state(cmd).results.iterator.map(_._2) filter {
     1.9                    case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
    1.10                    case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
    1.11                    case _ => true
    1.12                  }
    1.13 -              html_panel.render(filtered_results)
    1.14 +              html_panel.render(filtered_results.toList)
    1.15              case _ =>
    1.16            }
    1.17          case None =>