1.1 --- a/src/Pure/library.scala	Wed Jun 29 21:34:16 2011 +0200
     1.2 +++ b/src/Pure/library.scala	Wed Jun 29 23:43:48 2011 +0200
     1.3 @@ -13,11 +13,12 @@
     1.4  
     1.5  import scala.swing.ComboBox
     1.6  import scala.swing.event.SelectionChanged
     1.7 +import scala.collection.mutable
     1.8  
     1.9  
    1.10  object Library
    1.11  {
    1.12 -  /* separate */
    1.13 +  /* lists */
    1.14  
    1.15    def separate[A](s: A, list: List[A]): List[A] =
    1.16      list match {
    1.17 @@ -25,6 +26,27 @@
    1.18        case _ => list
    1.19      }
    1.20  
    1.21 +  def space_explode(sep: Char, str: String): List[String] =
    1.22 +    if (str.isEmpty) Nil
    1.23 +    else {
    1.24 +      val result = new mutable.ListBuffer[String]
    1.25 +      var start = 0
    1.26 +      var finished = false
    1.27 +      while (!finished) {
    1.28 +        val i = str.indexOf(sep, start)
    1.29 +        if (i == -1) { result += str.substring(start); finished = true }
    1.30 +        else { result += str.substring(start, i); start = i + 1 }
    1.31 +      }
    1.32 +      result.toList
    1.33 +    }
    1.34 +
    1.35 +
    1.36 +  /* strings */
    1.37 +
    1.38 +  def quote(s: String): String = "\"" + s + "\""
    1.39 +  def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
    1.40 +  def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
    1.41 +
    1.42  
    1.43    /* reverse CharSequence */
    1.44