# HG changeset patch
# User wenzelm
# Date 1326397888 -3600
# Node ID 872f915e3a98d0789a7b6e343359fd827efd457b
# Parent  55a4769d0abe917a7be900098e1150d1d8b41544
clarified mkString: no extra line-breaks for XML.Body;

diff -r 55a4769d0abe -r 872f915e3a98 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Jan 12 10:19:33 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Jan 12 20:51:28 2012 +0100
@@ -158,8 +158,7 @@
             val content = command.source(info.range).replace('\n', ' ')
             val info_text =
               info.info match {
-                case elem @ XML.Elem(_, _) =>
-                  Pretty.formatted(List(elem), margin = 40).mkString("\n")
+                case elem @ XML.Elem(_, _) => Pretty.formatted(List(elem), margin = 40).mkString
                 case x => x.toString
               }