clarified mkString: no extra line-breaks for XML.Body;

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