changeset 44331 | 8a6de1a6e1dc |
parent 44330 | 4b4b93672f15 |
child 44358 | 98cd7e83fc5b |
1.1 --- a/src/Pure/General/symbol.scala Sun Jun 19 14:11:06 2011 +0200 1.2 +++ b/src/Pure/General/symbol.scala Sun Jun 19 14:31:08 2011 +0200 1.3 @@ -230,7 +230,7 @@ 1.4 1.5 val names: Map[String, String] = 1.6 { 1.7 - val name = new Regex("""\\<([A-Za-z][A-Za-z0-9_']*)>""") 1.8 + val name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""") 1.9 Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*) 1.10 } 1.11