src/Pure/General/symbol.scala
changeset 44181 bbce0417236d
parent 43714 3749d1e6dde9
child 44238 36120feb70ed
equal deleted inserted replaced
44180:a6dc270d3edb 44181:bbce0417236d
   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 =