# HG changeset patch
# User wenzelm
# Date 1349989849 -7200
# Node ID 77582720af965b9e5cdcd6f52bd16af078a1d82a
# Parent  be66949288a2affe9707296e79704fde763b6bd8
refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;

diff -r be66949288a2 -r 77582720af96 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Oct 11 21:02:19 2012 +0200
+++ b/src/Pure/General/pretty.scala	Thu Oct 11 23:10:49 2012 +0200
@@ -59,7 +59,8 @@
 
   val FBreak = XML.Text("\n")
 
-  val Separator = XML.elem(Isabelle_Markup.SEPARATOR, List(FBreak))
+  val Separator = List(XML.elem(Isabelle_Markup.SEPARATOR, List(XML.Text(space))), FBreak)
+  def separate(ts: List[XML.Tree]): XML.Body = ts.map(t => t :: Separator).flatten
 
 
   /* formatted output */
diff -r be66949288a2 -r 77582720af96 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Oct 11 21:02:19 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Oct 11 23:10:49 2012 +0200
@@ -279,7 +279,7 @@
           case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), body)))
           if !body.isEmpty => msgs + (Document.new_id() -> msg)
         }).toList.flatMap(_.info)
-    Library.separate(Pretty.Separator, msgs.iterator.map(_._2).toList)
+    Pretty.separate(msgs.iterator.map(_._2).toList)
   }
 
 
diff -r be66949288a2 -r 77582720af96 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Thu Oct 11 21:02:19 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Oct 11 23:10:49 2012 +0200
@@ -84,7 +84,7 @@
       else (current_output, current_tracing)
 
     if (new_output != current_output)
-      pretty_text_area.update(new_snapshot, Library.separate(Pretty.Separator, new_output))
+      pretty_text_area.update(new_snapshot, Pretty.separate(new_output))
 
     if (new_tracing != current_tracing)
       tracing.text = tracing_text(new_tracing)