# HG changeset patch
# User wenzelm
# Date 1316464977 -7200
# Node ID aa34d2d049cecfbadb3def75b464ed7995710250
# Parent  d88f7fc62a405bcdb106f6b60c7fceaeec75678e
refined Symbol.is_symbolic -- cover recoded versions as well;

diff -r d88f7fc62a40 -r aa34d2d049ce src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Sep 19 22:13:51 2011 +0200
+++ b/src/Pure/General/symbol.scala	Mon Sep 19 22:42:57 2011 +0200
@@ -352,6 +352,8 @@
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
 
+    val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
+
 
     /* control symbols */
 
@@ -391,11 +393,16 @@
   def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'"
   def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
   def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
+
   def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
-  def is_symbolic(sym: Symbol): Boolean =
+  def is_symbolic(sym: Symbol): Boolean = raw_symbolic(sym) || symbols.symbolic.contains(sym)
+
+  private def raw_symbolic(sym: Symbol): Boolean =
     sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
 
 
+
+
   /* control symbols */
 
   def is_ctrl(sym: Symbol): Boolean =