changeset 43443 | 5d9693c2337e |
parent 43418 | c69e9fbb81a8 |
child 43447 | 0ef3ec385b2b |
--- a/src/Pure/General/symbol.scala Sat Jun 18 17:32:13 2011 +0200 +++ b/src/Pure/General/symbol.scala Sat Jun 18 17:33:27 2011 +0200 @@ -326,5 +326,7 @@ def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym) def is_symbolic(sym: String): Boolean = sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^") + def is_controllable(sym: String): Boolean = + !is_blank(sym) && !sym.startsWith("\\<^") } }