# HG changeset patch
# User wenzelm
# Date 1346237741 -7200
# Node ID a8bad1369adad98ebf06b5cad846ba81d72a4f65
# Parent  0e1cab4a334e9682a90fa23ff80b0af138a9fd47
clarified separated_chunks vs. space_explode;

diff -r 0e1cab4a334e -r a8bad1369ada src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Wed Aug 29 12:18:21 2012 +0200
+++ b/src/Pure/General/pretty.scala	Wed Aug 29 12:55:41 2012 +0200
@@ -65,9 +65,7 @@
   private def standard_format(tree: XML.Tree): XML.Body =
     tree match {
       case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(standard_format)))
-      case XML.Text(text) =>
-        Library.separate(FBreak,
-          Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
+      case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
     }
 
   private sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
diff -r 0e1cab4a334e -r a8bad1369ada src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Wed Aug 29 12:18:21 2012 +0200
+++ b/src/Pure/PIDE/yxml.scala	Wed Aug 29 12:55:41 2012 +0200
@@ -93,10 +93,10 @@
 
     /* parse chunks */
 
-    for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
+    for (chunk <- Library.separated_chunks(X, source) if chunk.length != 0) {
       if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
       else {
-        Library.chunks(chunk, Y).toList match {
+        Library.separated_chunks(Y, chunk).toList match {
           case ch :: name :: atts if ch.length == 0 =>
             push(name.toString, atts.map(parse_attrib))
           case txts => for (txt <- txts) add(XML.Text(txt.toString))
diff -r 0e1cab4a334e -r a8bad1369ada src/Pure/library.scala
--- 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(", ")