# 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 =