refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;

--- 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 */

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

--- 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)