# HG changeset patch
# User wenzelm
# Date 1273172554 -7200
# Node ID 2b3076cfd6ddb580112b346690bf8998b194f646
# Parent  943f1ca7b375762665d6e9b75a1e15fe8d1dab6c
slightly more general Library.chunks;

diff -r 943f1ca7b375 -r 2b3076cfd6dd src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Thu May 06 17:49:57 2010 +0200
+++ b/src/Pure/General/yxml.scala	Thu May 06 21:02:34 2010 +0200
@@ -20,29 +20,6 @@
   private val Y_string = Y.toString
 
 
-  /* iterate over chunks (resembles space_explode in ML) */
-
-  private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence]
-  {
-    private val end = source.length
-    private var state = if (end == 0) None else get_chunk(-1)
-    private def get_chunk(i: 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
-    }
-
-    def hasNext() = state.isDefined
-    def next() = state match {
-      case Some((s, i)) => { state = get_chunk(i); s }
-      case None => throw new NoSuchElementException("next on empty iterator")
-    }
-  }
-
-
   /* decoding pseudo UTF-8 */
 
   private class Decode_Chars(decode: String => String,
@@ -112,10 +89,10 @@
 
     /* parse chunks */
 
-    for (chunk <- chunks(X, source) if chunk.length != 0) {
+    for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
       if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
       else {
-        chunks(Y, chunk).toList match {
+        Library.chunks(chunk, Y).toList match {
           case ch :: name :: atts if ch.length == 0 =>
             push(name.toString.intern, atts.map(parse_attrib))
           case txts => for (txt <- txts) add(XML.Text(txt.toString))
diff -r 943f1ca7b375 -r 2b3076cfd6dd src/Pure/library.scala
--- a/src/Pure/library.scala	Thu May 06 17:49:57 2010 +0200
+++ b/src/Pure/library.scala	Thu May 06 21:02:34 2010 +0200
@@ -38,6 +38,30 @@
   }
 
 
+  /* iterate over chunks (cf. space_explode/split_lines in ML) */
+
+  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 => throw new NoSuchElementException("next on empty iterator")
+      }
+  }
+
+
   /* simple dialogs */
 
   private def simple_dialog(kind: Int, default_title: String)