# HG changeset patch # User wenzelm # Date 1347968188 -7200 # Node ID 8b402b550a80e4f14ad8952de247e72c2f722ae6 # Parent d7b5fb2e9ca20d2816cd340fb3331c17fac30080 proper separation of output messages; diff -r d7b5fb2e9ca2 -r 8b402b550a80 src/Tools/jEdit/src/output2_dockable.scala --- a/src/Tools/jEdit/src/output2_dockable.scala Tue Sep 18 13:18:45 2012 +0200 +++ b/src/Tools/jEdit/src/output2_dockable.scala Tue Sep 18 13:36:28 2012 +0200 @@ -32,7 +32,7 @@ private var show_tracing = false private var do_update = true private var current_state = Command.empty.init_state - private var current_body: XML.Body = Nil + private var current_output: List[XML.Tree] = Nil /* pretty text panel */ @@ -67,19 +67,20 @@ } else current_state - val new_body = + val new_output = if (!restriction.isDefined || restriction.get.contains(new_state.command)) new_state.results.iterator.map(_._2).filter( { // FIXME not scalable case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing case _ => true }).toList - else current_body + else current_output - if (new_body != current_body) pretty_text_area.update(new_body) + if (new_output != current_output) + pretty_text_area.update(Library.separate(Pretty.FBreak, new_output)) current_state = new_state - current_body = new_body + current_output = new_output }