equal
deleted
inserted
replaced
253 var tab = Map[String, String]() |
253 var tab = Map[String, String]() |
254 for ((x, y) <- list) { |
254 for ((x, y) <- list) { |
255 tab.get(x) match { |
255 tab.get(x) match { |
256 case None => tab += (x -> y) |
256 case None => tab += (x -> y) |
257 case Some(z) => |
257 case Some(z) => |
258 error("Duplicate mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z)) |
258 error("Duplicate symbol mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z)) |
259 } |
259 } |
260 } |
260 } |
261 tab |
261 tab |
262 } |
262 } |
263 def recode(text: String): String = |
263 def recode(text: String): String = |