equal
deleted
inserted
replaced
98 } |
98 } |
99 else current_state |
99 else current_state |
100 |
100 |
101 val new_body = |
101 val new_body = |
102 if (!restriction.isDefined || restriction.get.contains(new_state.command)) |
102 if (!restriction.isDefined || restriction.get.contains(new_state.command)) |
103 new_state.results.iterator.map(_._2).filter( |
103 new_state.results.iterator.map(_._2) |
104 { // FIXME not scalable |
104 .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList // FIXME not scalable |
105 case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing |
|
106 case _ => true |
|
107 }).toList |
|
108 else current_body |
105 else current_body |
109 |
106 |
110 if (new_body != current_body) html_panel.render(new_body) |
107 if (new_body != current_body) html_panel.render(new_body) |
111 |
108 |
112 current_state = new_state |
109 current_state = new_state |