src/Tools/jEdit/src/isabelle_rendering.scala

             markup == Isabelle_Markup.ERROR =>
           msgs + (serial ->
             Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
       }) match {
         case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
-          Some(msgs.iterator.map(_._2).mkString("\n"))
+          Some(cat_lines(msgs.iterator.map(_._2)))
         case _ => None
       }
 
   def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
   {

 
     val tips =
       (tip1 match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil }) :::
       (tip2 match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil })
 
-    if (tips.isEmpty) None else Some(tips.mkString("\n"))
+    if (tips.isEmpty) None else Some(cat_lines(tips))
   }
 
   private val subexp_include =
     Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
       Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,