# HG changeset patch
# User wenzelm
# Date 1326398297 -3600
# Node ID 805de058722bbb49bc762fc35eb55f638a89ca9d
# Parent  d4558296bdc3dff2eb9ce03d0306d370dc023896
added cat_lines convenience;

diff -r d4558296bdc3 -r 805de058722b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Jan 12 20:57:37 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Jan 12 20:58:17 2012 +0100
@@ -120,7 +120,7 @@
   def current_syntax(): Outer_Syntax = syntax
 
   @volatile private var reverse_syslog = List[XML.Elem]()
-  def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
+  def syslog(): String = cat_lines(reverse_syslog.reverse.map(msg => XML.content(msg).mkString))
 
   @volatile private var _phase: Session.Phase = Session.Inactive
   private def phase_=(new_phase: Session.Phase)
diff -r d4558296bdc3 -r 805de058722b src/Pure/library.scala
--- a/src/Pure/library.scala	Thu Jan 12 20:57:37 2012 +0100
+++ b/src/Pure/library.scala	Thu Jan 12 20:58:17 2012 +0100
@@ -98,6 +98,8 @@
 
   /* strings */
 
+  def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
+
   def quote(s: String): String = "\"" + s + "\""
   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
   def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
@@ -208,7 +210,7 @@
 
   val space_explode = Library.space_explode _
   val split_lines = Library.split_lines _
-
+  val cat_lines = Library.cat_lines _
   val quote = Library.quote _
   val commas = Library.commas _
   val commas_quote = Library.commas_quote _
diff -r d4558296bdc3 -r 805de058722b src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Jan 12 20:57:37 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Jan 12 20:58:17 2012 +0100
@@ -102,7 +102,7 @@
             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
       }
 
@@ -256,7 +256,7 @@
       (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 =