# HG changeset patch
# User wenzelm
# Date 1309383828 -7200
# Node ID 826ddd91ae2b6e59e9a043b90ed58df82b60a370
# Parent  b4a093e755db050666fe348217ed4f7b549887ce
basic operations on lists and strings;

diff -r b4a093e755db -r 826ddd91ae2b src/Pure/library.scala
--- a/src/Pure/library.scala	Wed Jun 29 21:34:16 2011 +0200
+++ b/src/Pure/library.scala	Wed Jun 29 23:43:48 2011 +0200
@@ -13,11 +13,12 @@
 
 import scala.swing.ComboBox
 import scala.swing.event.SelectionChanged
+import scala.collection.mutable
 
 
 object Library
 {
-  /* separate */
+  /* lists */
 
   def separate[A](s: A, list: List[A]): List[A] =
     list match {
@@ -25,6 +26,27 @@
       case _ => list
     }
 
+  def space_explode(sep: Char, str: String): List[String] =
+    if (str.isEmpty) Nil
+    else {
+      val result = new mutable.ListBuffer[String]
+      var start = 0
+      var finished = false
+      while (!finished) {
+        val i = str.indexOf(sep, start)
+        if (i == -1) { result += str.substring(start); finished = true }
+        else { result += str.substring(start, i); start = i + 1 }
+      }
+      result.toList
+    }
+
+
+  /* strings */
+
+  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("\"", ", ", "\"")
+
 
   /* reverse CharSequence */