tuned;
authorwenzelm
Mon, 06 Mar 2017 17:05:57 +0100
changeset 65130 695930882487
parent 65129 06a7c2d316cf
child 65131 5d35f4bccfa7
tuned;
src/Pure/General/pretty.scala
src/Tools/jEdit/src/isabelle_sidekick.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
--- 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) {