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