1.1 --- a/src/Pure/library.scala	Tue Jul 05 21:20:24 2011 +0200
     1.2 +++ b/src/Pure/library.scala	Tue Jul 05 21:32:48 2011 +0200
     1.3 @@ -61,6 +61,8 @@
     1.4        result.toList
     1.5      }
     1.6  
     1.7 +  def split_lines(str: String): List[String] = space_explode('\n', str)
     1.8 +
     1.9  
    1.10    /* iterate over chunks (cf. space_explode) */
    1.11  
    1.12 @@ -185,13 +187,14 @@
    1.13  
    1.14  class Basic_Library
    1.15  {
    1.16 +  val ERROR = Library.ERROR
    1.17 +  val error = Library.error _
    1.18 +  val cat_error = Library.cat_error _
    1.19 +
    1.20    val space_explode = Library.space_explode _
    1.21 +  val split_lines = Library.split_lines _
    1.22  
    1.23    val quote = Library.quote _
    1.24    val commas = Library.commas _
    1.25    val commas_quote = Library.commas_quote _
    1.26 -
    1.27 -  val ERROR = Library.ERROR
    1.28 -  val error = Library.error _
    1.29 -  val cat_error = Library.cat_error _
    1.30  }