# HG changeset patch
# User wenzelm
# Date 1289245856 -3600
# Node ID 41c32616298c885867002c2b4b15a139bd281cf5
# Parent  19faffbe50660b3e2e77bedb33e65e8d520e6124
explicitly check uniqueness of symbol recoding;

diff -r 19faffbe5066 -r 41c32616298c src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Nov 08 17:44:47 2010 +0100
+++ b/src/Pure/General/symbol.scala	Mon Nov 08 20:50:56 2010 +0100
@@ -146,7 +146,18 @@
       }
       (min, max)
     }
-    private val table = Map[String, String]() ++ list
+    private val table =
+    {
+      var tab = Map[String, String]()
+      for ((x, y) <- list) {
+        tab.get(x) match {
+          case None => tab += (x -> y)
+          case Some(z) =>
+            error("Duplicate mapping of \"" + x + "\" to \"" + y + "\" vs. \"" + z + "\"")
+        }
+      }
+      tab
+    }
     def recode(text: String): String =
     {
       val len = text.length
@@ -198,8 +209,9 @@
     }
 
     private val symbols: List[(String, Map[String, String])] =
-      for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
-        yield read_decl(decl)
+      Map((
+        for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
+          yield read_decl(decl)): _*) toList
 
 
     /* misc properties */
@@ -210,9 +222,10 @@
       Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
     }
 
-    val abbrevs: Map[String, String] = Map((
-      for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
-        yield (sym -> props("abbrev"))): _*)
+    val abbrevs: Map[String, String] =
+      Map((
+        for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
+          yield (sym -> props("abbrev"))): _*)
 
 
     /* main recoder methods */