# HG changeset patch
# User wenzelm
# Date 1418035744 -3600
# Node ID 48429ad6d0c82c4e16d800605c67b2b73bf01943
# Parent  a14475f044b2856ddbe7ebb3e8946ea359644bb4
tuned signature;

diff -r a14475f044b2 -r 48429ad6d0c8 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Dec 05 19:35:36 2014 +0100
+++ b/src/Pure/General/symbol.scala	Mon Dec 08 11:49:04 2014 +0100
@@ -438,7 +438,7 @@
 
     /* control symbols */
 
-    val ctrl_decoded: Set[Symbol] =
+    val control_decoded: Set[Symbol] =
       Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
 
     val sub_decoded = decode("\\<^sub>")
@@ -516,11 +516,11 @@
 
   /* control symbols */
 
-  def is_ctrl(sym: Symbol): Boolean =
-    sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym)
+  def is_control(sym: Symbol): Boolean =
+    sym.startsWith("\\<^") || symbols.control_decoded.contains(sym)
 
   def is_controllable(sym: Symbol): Boolean =
-    !is_blank(sym) && !is_ctrl(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym)
+    !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym)
 
   def sub_decoded: Symbol = symbols.sub_decoded
   def sup_decoded: Symbol = symbols.sup_decoded