src/Pure/General/symbol.scala
changeset 62230 949d2c9f6ff7
parent 62104 fb73c0d7bb37
child 62528 c8c532b22947
equal deleted inserted replaced
62229:027e6032977f 62230:949d2c9f6ff7
   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 =