--- a/src/Pure/library.scala Wed Aug 29 12:18:21 2012 +0200
+++ b/src/Pure/library.scala Wed Aug 29 12:55:41 2012 +0200
@@ -34,7 +34,7 @@
else error(msg1 + "\n" + msg2)
- /* lists */
+ /* separated chunks */
def separate[A](s: A, list: List[A]): List[A] =
list match {
@@ -42,61 +42,50 @@
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 }
+ def separated_chunks(sep: Char, source: CharSequence): Iterator[CharSequence] =
+ new Iterator[CharSequence] {
+ private val end = source.length
+ private def next_chunk(i: Int): Option[(CharSequence, Int)] =
+ {
+ if (i < end) {
+ var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
+ Some((source.subSequence(i + 1, j), j))
+ }
+ else None
}
- result.toList
+ private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
+
+ def hasNext(): Boolean = state.isDefined
+ def next(): CharSequence =
+ state match {
+ case Some((s, i)) => { state = next_chunk(i); s }
+ case None => Iterator.empty.next()
+ }
}
+ def space_explode(sep: Char, str: String): List[String] =
+ separated_chunks(sep, str).map(_.toString).toList
+
+
+ /* lines */
+
+ def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
+
def split_lines(str: String): List[String] = space_explode('\n', str)
+ def first_line(source: CharSequence): String =
+ {
+ val lines = separated_chunks('\n', source)
+ if (lines.hasNext) lines.next.toString
+ else ""
+ }
+
def trim_line(str: String): String =
if (str.endsWith("\n")) str.substring(0, str.length - 1)
else str
- /* iterate over chunks (cf. space_explode) */
-
- def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
- {
- private val end = source.length
- private def next_chunk(i: Int): Option[(CharSequence, Int)] =
- {
- if (i < end) {
- var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
- Some((source.subSequence(i + 1, j), j))
- }
- else None
- }
- private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
-
- def hasNext(): Boolean = state.isDefined
- def next(): CharSequence =
- state match {
- case Some((s, i)) => { state = next_chunk(i); s }
- case None => Iterator.empty.next()
- }
- }
-
- def first_line(source: CharSequence): String =
- {
- val lines = chunks(source)
- if (lines.hasNext) lines.next.toString
- else ""
- }
-
-
- /* strings */
-
- def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
+ /* quote */
def quote(s: String): String = "\"" + s + "\""
def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")