equal
deleted
inserted
replaced
106 if (str == "") str else cat_lines(split_lines(str).map(prfx + _)) |
106 if (str == "") str else cat_lines(split_lines(str).map(prfx + _)) |
107 |
107 |
108 def first_line(source: CharSequence): String = |
108 def first_line(source: CharSequence): String = |
109 { |
109 { |
110 val lines = separated_chunks(_ == '\n', source) |
110 val lines = separated_chunks(_ == '\n', source) |
111 if (lines.hasNext) lines.next.toString |
111 if (lines.hasNext) lines.next().toString |
112 else "" |
112 else "" |
113 } |
113 } |
114 |
114 |
115 def trim_line(s: String): String = |
115 def trim_line(s: String): String = |
116 if (s.endsWith("\r\n")) s.substring(0, s.length - 2) |
116 if (s.endsWith("\r\n")) s.substring(0, s.length - 2) |