changeset 43447 | 0ef3ec385b2b |
parent 43443 | 5d9693c2337e |
child 43455 | 4b4b93672f15 |
--- 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) } }