1.1 --- a/src/Pure/General/symbol.scala	Mon Sep 19 22:13:51 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Mon Sep 19 22:42:57 2011 +0200
     1.3 @@ -352,6 +352,8 @@
     1.4      val sym_chars =
     1.5        Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
     1.6  
     1.7 +    val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
     1.8 +
     1.9  
    1.10      /* control symbols */
    1.11  
    1.12 @@ -391,11 +393,16 @@
    1.13    def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'"
    1.14    def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
    1.15    def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
    1.16 +
    1.17    def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
    1.18 -  def is_symbolic(sym: Symbol): Boolean =
    1.19 +  def is_symbolic(sym: Symbol): Boolean = raw_symbolic(sym) || symbols.symbolic.contains(sym)
    1.20 +
    1.21 +  private def raw_symbolic(sym: Symbol): Boolean =
    1.22      sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
    1.23  
    1.24  
    1.25 +
    1.26 +
    1.27    /* control symbols */
    1.28  
    1.29    def is_ctrl(sym: Symbol): Boolean =