# HG changeset patch
# User wenzelm
# Date 1262004030 -3600
# Node ID d3358b909c40f6a4642e8c94f6188be128bba13b
# Parent  619552fe8d7fd583f0a4940c24f70db54582a5a9
some sanity checks for symbol interpretation;

diff -r 619552fe8d7f -r d3358b909c40 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sun Dec 27 23:10:03 2009 +0100
+++ b/src/Pure/General/symbol.scala	Mon Dec 28 13:40:30 2009 +0100
@@ -177,8 +177,8 @@
         }
       }
       decl.split("\\s+").toList match {
-        case Nil => err()
-        case sym :: props => (sym, read_props(props))
+        case sym :: props if sym.length > 1 && is_closed(sym) => (sym, read_props(props))
+        case _ => err()
       }
     }
 
@@ -214,7 +214,10 @@
               case _: NumberFormatException => error("Bad code for symbol " + sym)
             }
           val ch = new String(Character.toChars(code))
-        } yield (sym, ch)
+        } yield {
+          if (code < 128) error("Illegal ASCII code for symbol " + sym)
+          else (sym, ch)
+        }
       (new Recoder(mapping),
        new Recoder(mapping map { case (x, y) => (y, x) }))
     }