# HG changeset patch
# User wenzelm
# Date 1488816357 -3600
# Node ID 695930882487fc981154279a7ceeb151d01ca6bb
# Parent  06a7c2d316cf0857fe2f65882f06703677a1925b
tuned;

diff -r 06a7c2d316cf -r 695930882487 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Mon Mar 06 16:47:52 2017 +0100
+++ b/src/Pure/General/pretty.scala	Mon Mar 06 17:05:57 2017 +0100
@@ -26,6 +26,7 @@
     XML.Elem(Markup.Break(width, indent), spaces(width))
 
   val fbrk: XML.Tree = XML.Text("\n")
+  def fbreaks(ts: List[XML.Tree]): XML.Body = Library.separate(fbrk, ts)
 
   val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)
   def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
diff -r 06a7c2d316cf -r 695930882487 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Mar 06 16:47:52 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Mar 06 17:05:57 2017 +0100
@@ -194,9 +194,7 @@
               {
                 val range = info.range + command_start
                 val content = command.source(info.range).replace('\n', ' ')
-                val info_text =
-                  Pretty.formatted(Library.separate(Pretty.fbrk, info.info), margin = 40.0)
-                    .mkString
+                val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString
 
                 new DefaultMutableTreeNode(
                   new Isabelle_Sidekick.Asset(command.toString, range) {