equal
deleted
inserted
replaced
60 result.toList |
60 result.toList |
61 } |
61 } |
62 |
62 |
63 def split_lines(str: String): List[String] = space_explode('\n', str) |
63 def split_lines(str: String): List[String] = space_explode('\n', str) |
64 |
64 |
|
65 def trim_line(str: String): String = |
|
66 if (str.endsWith("\n")) str.substring(0, str.length - 1) |
|
67 else str |
|
68 |
65 |
69 |
66 /* iterate over chunks (cf. space_explode) */ |
70 /* iterate over chunks (cf. space_explode) */ |
67 |
71 |
68 def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence] |
72 def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence] |
69 { |
73 { |