equal
deleted
inserted
replaced
140 else s |
140 else s |
141 |
141 |
142 def trim_split_lines(s: String): List[String] = |
142 def trim_split_lines(s: String): List[String] = |
143 split_lines(trim_line(s)).map(trim_line(_)) |
143 split_lines(trim_line(s)).map(trim_line(_)) |
144 |
144 |
145 def trim_substring(s: String): String = new String(s.toCharArray) |
145 def isolate_substring(s: String): String = new String(s.toCharArray) |
146 |
146 |
147 |
147 |
148 /* quote */ |
148 /* quote */ |
149 |
149 |
150 def quote(s: String): String = "\"" + s + "\"" |
150 def quote(s: String): String = "\"" + s + "\"" |