1.1 --- a/src/Pure/General/symbol.scala	Sat Dec 19 16:51:32 2009 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Sun Dec 20 15:41:57 2009 +0100
     1.3 @@ -32,13 +32,13 @@
     1.4  
     1.5    /* basic matching */
     1.6  
     1.7 -  def is_open(c: Char): Boolean =
     1.8 -    c == '\\' || Character.isHighSurrogate(c)
     1.9 +  def is_closed(c: Char): Boolean =
    1.10 +    !(c == '\\' || Character.isHighSurrogate(c))
    1.11  
    1.12 -  def is_open(s: CharSequence): Boolean =
    1.13 +  def is_closed(s: CharSequence): Boolean =
    1.14    {
    1.15 -    if (s.length == 1) is_open(s.charAt(0))
    1.16 -    else bad_symbol.pattern.matcher(s).matches
    1.17 +    if (s.length == 1) is_closed(s.charAt(0))
    1.18 +    else !bad_symbol.pattern.matcher(s).matches
    1.19    }
    1.20  
    1.21    class Matcher(text: CharSequence)
    1.22 @@ -47,11 +47,11 @@
    1.23      def apply(start: Int, end: Int): Int =
    1.24      {
    1.25        require(0 <= start && start < end && end <= text.length)
    1.26 -      if (is_open(text.charAt(start))) {
    1.27 +      if (is_closed(text.charAt(start))) 1
    1.28 +      else {
    1.29          matcher.region(start, end).lookingAt
    1.30          matcher.group.length
    1.31        }
    1.32 -      else 1
    1.33      }
    1.34    }
    1.35  
    1.36 @@ -225,7 +225,16 @@
    1.37  
    1.38      /* classification */
    1.39  
    1.40 -    private val raw_letters = Set(
    1.41 +    private object Decode_Set
    1.42 +    {
    1.43 +      def apply(elems: String*): Set[String] =
    1.44 +      {
    1.45 +        val content = elems.toList
    1.46 +        Set((content ::: content.map(decode)): _*)
    1.47 +      }
    1.48 +    }
    1.49 +
    1.50 +    private val letters = Decode_Set(
    1.51        "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
    1.52        "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
    1.53        "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
    1.54 @@ -260,24 +269,18 @@
    1.55  
    1.56        "\\<^isub>", "\\<^isup>")
    1.57  
    1.58 -    private val letters = raw_letters ++ raw_letters.map(decode(_))
    1.59 +    private val blanks =
    1.60 +      Decode_Set(" ", "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
    1.61 +
    1.62 +    private val sym_chars =
    1.63 +      Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
    1.64  
    1.65      def is_letter(sym: String): Boolean = letters.contains(sym)
    1.66 -
    1.67 -    def is_digit(sym: String): Boolean =
    1.68 -      if (sym.length == 1) {
    1.69 -        val c = sym(0)
    1.70 -        '0' <= c && c <= '9'
    1.71 -      }
    1.72 -      else false
    1.73 -
    1.74 +    def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
    1.75      def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
    1.76 -
    1.77 -
    1.78 -    private val raw_blanks =
    1.79 -      Set(" ", "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
    1.80 -    private val blanks = raw_blanks ++ raw_blanks.map(decode(_))
    1.81 -
    1.82 +    def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
    1.83      def is_blank(sym: String): Boolean = blanks.contains(sym)
    1.84 +    def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym)
    1.85 +    def is_symbolic(sym: String): Boolean = sym.startsWith("\\<") && !sym.startsWith("\\<^")
    1.86    }
    1.87  }