equal
deleted
inserted
replaced
177 var tab = Map[String, String]() |
177 var tab = Map[String, String]() |
178 for ((x, y) <- list) { |
178 for ((x, y) <- list) { |
179 tab.get(x) match { |
179 tab.get(x) match { |
180 case None => tab += (x -> y) |
180 case None => tab += (x -> y) |
181 case Some(z) => |
181 case Some(z) => |
182 error("Duplicate mapping of \"" + x + "\" to \"" + y + "\" vs. \"" + z + "\"") |
182 error("Duplicate mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z)) |
183 } |
183 } |
184 } |
184 } |
185 tab |
185 tab |
186 } |
186 } |
187 def recode(text: String): String = |
187 def recode(text: String): String = |