equal
deleted
inserted
replaced
67 } |
67 } |
68 else current_state |
68 else current_state |
69 |
69 |
70 val new_output = |
70 val new_output = |
71 if (!restriction.isDefined || restriction.get.contains(new_state.command)) |
71 if (!restriction.isDefined || restriction.get.contains(new_state.command)) |
72 new_state.results.iterator.map(_._2).filter( |
72 new_state.results.iterator.map(_._2) |
73 { // FIXME not scalable |
73 .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList // FIXME not scalable |
74 case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing |
|
75 case _ => true |
|
76 }).toList |
|
77 else current_output |
74 else current_output |
78 |
75 |
79 if (new_output != current_output) |
76 if (new_output != current_output) |
80 pretty_text_area.update(Library.separate(Pretty.FBreak, new_output)) |
77 pretty_text_area.update(Library.separate(Pretty.FBreak, new_output)) |
81 |
78 |