src/Pure/General/symbol.scala
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("\\<^")
   }
 }