equal
deleted
inserted
replaced
84 case Some(doc_view) => |
84 case Some(doc_view) => |
85 current_command match { |
85 current_command match { |
86 case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => |
86 case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => |
87 val snapshot = doc_view.update_snapshot() |
87 val snapshot = doc_view.update_snapshot() |
88 val filtered_results = |
88 val filtered_results = |
89 snapshot.command_state(cmd).results.iterator.map(_._2) filter { |
89 snapshot.state.command_state(snapshot.version, cmd).results.iterator |
90 case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing // FIXME not scalable |
90 .map(_._2).filter( |
91 case _ => true |
91 { // FIXME not scalable |
92 } |
92 case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing |
93 html_panel.render(filtered_results.toList) |
93 case _ => true |
|
94 }).toList |
|
95 html_panel.render(filtered_results) |
94 case _ => |
96 case _ => |
95 } |
97 } |
96 case None => |
98 case None => |
97 } |
99 } |
98 } |
100 } |