32 def cat_error(msg1: String, msg2: String): Nothing = |
32 def cat_error(msg1: String, msg2: String): Nothing = |
33 if (msg1 == "") error(msg1) |
33 if (msg1 == "") error(msg1) |
34 else error(msg1 + "\n" + msg2) |
34 else error(msg1 + "\n" + msg2) |
35 |
35 |
36 |
36 |
37 /* lists */ |
37 /* separated chunks */ |
38 |
38 |
39 def separate[A](s: A, list: List[A]): List[A] = |
39 def separate[A](s: A, list: List[A]): List[A] = |
40 list match { |
40 list match { |
41 case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs) |
41 case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs) |
42 case _ => list |
42 case _ => list |
43 } |
43 } |
44 |
44 |
45 def space_explode(sep: Char, str: String): List[String] = |
45 def separated_chunks(sep: Char, source: CharSequence): Iterator[CharSequence] = |
46 if (str.isEmpty) Nil |
46 new Iterator[CharSequence] { |
47 else { |
47 private val end = source.length |
48 val result = new mutable.ListBuffer[String] |
48 private def next_chunk(i: Int): Option[(CharSequence, Int)] = |
49 var start = 0 |
49 { |
50 var finished = false |
50 if (i < end) { |
51 while (!finished) { |
51 var j = i; do j += 1 while (j < end && source.charAt(j) != sep) |
52 val i = str.indexOf(sep, start) |
52 Some((source.subSequence(i + 1, j), j)) |
53 if (i == -1) { result += str.substring(start); finished = true } |
53 } |
54 else { result += str.substring(start, i); start = i + 1 } |
54 else None |
55 } |
55 } |
56 result.toList |
56 private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1) |
|
57 |
|
58 def hasNext(): Boolean = state.isDefined |
|
59 def next(): CharSequence = |
|
60 state match { |
|
61 case Some((s, i)) => { state = next_chunk(i); s } |
|
62 case None => Iterator.empty.next() |
|
63 } |
57 } |
64 } |
58 |
65 |
|
66 def space_explode(sep: Char, str: String): List[String] = |
|
67 separated_chunks(sep, str).map(_.toString).toList |
|
68 |
|
69 |
|
70 /* lines */ |
|
71 |
|
72 def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n") |
|
73 |
59 def split_lines(str: String): List[String] = space_explode('\n', str) |
74 def split_lines(str: String): List[String] = space_explode('\n', str) |
|
75 |
|
76 def first_line(source: CharSequence): String = |
|
77 { |
|
78 val lines = separated_chunks('\n', source) |
|
79 if (lines.hasNext) lines.next.toString |
|
80 else "" |
|
81 } |
60 |
82 |
61 def trim_line(str: String): String = |
83 def trim_line(str: String): String = |
62 if (str.endsWith("\n")) str.substring(0, str.length - 1) |
84 if (str.endsWith("\n")) str.substring(0, str.length - 1) |
63 else str |
85 else str |
64 |
86 |
65 |
87 |
66 /* iterate over chunks (cf. space_explode) */ |
88 /* quote */ |
67 |
|
68 def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence] |
|
69 { |
|
70 private val end = source.length |
|
71 private def next_chunk(i: Int): Option[(CharSequence, Int)] = |
|
72 { |
|
73 if (i < end) { |
|
74 var j = i; do j += 1 while (j < end && source.charAt(j) != sep) |
|
75 Some((source.subSequence(i + 1, j), j)) |
|
76 } |
|
77 else None |
|
78 } |
|
79 private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1) |
|
80 |
|
81 def hasNext(): Boolean = state.isDefined |
|
82 def next(): CharSequence = |
|
83 state match { |
|
84 case Some((s, i)) => { state = next_chunk(i); s } |
|
85 case None => Iterator.empty.next() |
|
86 } |
|
87 } |
|
88 |
|
89 def first_line(source: CharSequence): String = |
|
90 { |
|
91 val lines = chunks(source) |
|
92 if (lines.hasNext) lines.next.toString |
|
93 else "" |
|
94 } |
|
95 |
|
96 |
|
97 /* strings */ |
|
98 |
|
99 def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n") |
|
100 |
89 |
101 def quote(s: String): String = "\"" + s + "\"" |
90 def quote(s: String): String = "\"" + s + "\"" |
102 def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ") |
91 def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ") |
103 def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ") |
92 def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ") |
104 |
93 |