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