# HG changeset patch
# User wenzelm
# Date 1308486668 -7200
# Node ID 8a6de1a6e1dc6eeb6978d29171f0056d37badf79
# Parent  4b4b93672f15dae0f6047b67f281ef020c9626c2
names for control symbols without "^", which is relevant for completion;

diff -r 4b4b93672f15 -r 8a6de1a6e1dc src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sun Jun 19 14:11:06 2011 +0200
+++ b/src/Pure/General/symbol.scala	Sun Jun 19 14:31:08 2011 +0200
@@ -230,7 +230,7 @@
 
     val names: Map[String, String] =
     {
-      val name = new Regex("""\\<([A-Za-z][A-Za-z0-9_']*)>""")
+      val name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
       Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
     }