--- a/src/Pure/General/symbol.scala Mon Aug 25 16:52:11 2008 +0200
+++ b/src/Pure/General/symbol.scala Mon Aug 25 20:01:17 2008 +0200
@@ -81,8 +81,6 @@
class Interpretation {
- class BadSymbol(val msg: String) extends Exception
-
private var symbols = new HashMap[String, HashMap[String, String]]
private var decoder: Recoder = null
private var encoder: Recoder = null
@@ -98,7 +96,7 @@
private val key_pattern = compile(""" (.+): """)
private def read_line(line: String) = {
- def err() = throw new BadSymbol(line)
+ def err() = error("Bad symbol specification (line " + line + ")")
def read_props(props: List[String], tab: HashMap[String, String]): Unit = {
props match {
@@ -142,8 +140,8 @@
val code =
try { Integer.decode(props("code")).intValue }
catch {
- case e: NoSuchElementException => throw new BadSymbol(symbol)
- case e: NumberFormatException => throw new BadSymbol(symbol)
+ case _: NoSuchElementException => error("Missing code for symbol " + symbol)
+ case _: NumberFormatException => error("Bad code for symbol " + symbol)
}
(symbol, new String(Character.toChars(code)))
}