--- a/src/Pure/library.scala Tue May 14 14:17:56 2013 +0200
+++ b/src/Pure/library.scala Tue May 14 15:40:18 2013 +0200
@@ -77,6 +77,12 @@
/* lines */
+ def terminate_lines(lines: Iterable[CharSequence]): Iterable[CharSequence] =
+ new Iterable[CharSequence] {
+ def iterator: Iterator[CharSequence] =
+ lines.iterator.map(line => new Line_Termination(line))
+ }
+
def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
def split_lines(str: String): List[String] = space_explode('\n', str)
@@ -109,7 +115,7 @@
def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
- /* reverse CharSequence */
+ /* CharSequence */
class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
{
@@ -133,6 +139,16 @@
}
}
+ class Line_Termination(text: CharSequence) extends CharSequence
+ {
+ def length: Int = text.length + 1
+ def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
+ def subSequence(i: Int, j: Int): CharSequence =
+ if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
+ else text.subSequence(i, j)
+ override def toString: String = text.toString + "\n"
+ }
+
/* Java futures */