# HG changeset patch
# User wenzelm
# Date 1308416258 -7200
# Node ID 0ef3ec385b2b14cba7f9b5796250a27e26c3f896
# Parent  9064e1a72c5d277a2e6cf040d76a9fe0754184b6
do not control malformed symbols;

diff -r 9064e1a72c5d -r 0ef3ec385b2b src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat Jun 18 18:31:55 2011 +0200
+++ b/src/Pure/General/symbol.scala	Sat Jun 18 18:57:38 2011 +0200
@@ -327,6 +327,6 @@
     def is_symbolic(sym: String): Boolean =
       sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
     def is_controllable(sym: String): Boolean =
-      !is_blank(sym) && !sym.startsWith("\\<^")
+      !is_blank(sym) && !sym.startsWith("\\<^") && !is_malformed(sym)
   }
 }