src/Pure/library.scala
changeset 47067 805de058722b
parent 46773 793bf5fa5fbf
child 47531 e16029f695ac
     1.1 --- a/src/Pure/library.scala	Thu Jan 12 20:57:37 2012 +0100
     1.2 +++ b/src/Pure/library.scala	Thu Jan 12 20:58:17 2012 +0100
     1.3 @@ -98,6 +98,8 @@
     1.4  
     1.5    /* strings */
     1.6  
     1.7 +  def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
     1.8 +
     1.9    def quote(s: String): String = "\"" + s + "\""
    1.10    def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
    1.11    def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
    1.12 @@ -208,7 +210,7 @@
    1.13  
    1.14    val space_explode = Library.space_explode _
    1.15    val split_lines = Library.split_lines _
    1.16 -
    1.17 +  val cat_lines = Library.cat_lines _
    1.18    val quote = Library.quote _
    1.19    val commas = Library.commas _
    1.20    val commas_quote = Library.commas_quote _