--- a/src/Pure/General/symbol.scala Mon Dec 04 16:28:06 2017 +0100
+++ b/src/Pure/General/symbol.scala Mon Dec 04 17:37:26 2017 +0100
@@ -577,8 +577,14 @@
/* control symbols */
+ val control_prefix = "\\<^"
+ val control_suffix = ">"
+
+ def is_control_encoded(sym: Symbol): Boolean =
+ sym.startsWith(control_prefix) && sym.endsWith(control_suffix)
+
def is_control(sym: Symbol): Boolean =
- (sym.startsWith("\\<^") && sym.endsWith(">")) || symbols.control_decoded.contains(sym)
+ is_control_encoded(sym) || symbols.control_decoded.contains(sym)
def is_controllable(sym: Symbol): Boolean =
!is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) &&