# 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
   }