1.1 --- a/src/Pure/General/symbol.scala	Sat Dec 19 16:02:26 2009 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Sat Dec 19 16:51:32 2009 +0100
     1.3 @@ -29,37 +29,45 @@
     1.4    // total pattern
     1.5    val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
     1.6  
     1.7 -  // prefix of another symbol
     1.8 +
     1.9 +  /* basic matching */
    1.10 +
    1.11 +  def is_open(c: Char): Boolean =
    1.12 +    c == '\\' || Character.isHighSurrogate(c)
    1.13 +
    1.14    def is_open(s: CharSequence): Boolean =
    1.15    {
    1.16 -    val len = s.length
    1.17 -    len == 1 && Character.isHighSurrogate(s.charAt(0)) ||
    1.18 -    s == "\\" ||
    1.19 -    s == "\\<" ||
    1.20 -    len > 2 && s.charAt(len - 1) != '>'   // FIXME bad_symbol !??
    1.21 +    if (s.length == 1) is_open(s.charAt(0))
    1.22 +    else bad_symbol.pattern.matcher(s).matches
    1.23 +  }
    1.24 +
    1.25 +  class Matcher(text: CharSequence)
    1.26 +  {
    1.27 +    private val matcher = regex.pattern.matcher(text)
    1.28 +    def apply(start: Int, end: Int): Int =
    1.29 +    {
    1.30 +      require(0 <= start && start < end && end <= text.length)
    1.31 +      if (is_open(text.charAt(start))) {
    1.32 +        matcher.region(start, end).lookingAt
    1.33 +        matcher.group.length
    1.34 +      }
    1.35 +      else 1
    1.36 +    }
    1.37    }
    1.38  
    1.39  
    1.40    /* elements */
    1.41  
    1.42 -  def could_open(c: Char): Boolean =
    1.43 -    c == '\\' || Character.isHighSurrogate(c)
    1.44 -
    1.45 -  def elements(text: CharSequence) = new Iterator[String]
    1.46 +  def elements(text: CharSequence) = new Iterator[CharSequence]
    1.47    {
    1.48 -    private val matcher = regex.pattern.matcher(text)
    1.49 +    private val matcher = new Matcher(text)
    1.50      private var i = 0
    1.51      def hasNext = i < text.length
    1.52      def next = {
    1.53 -      val len =
    1.54 -        if (could_open(text.charAt(i))) {
    1.55 -          matcher.region(i, text.length).lookingAt
    1.56 -          matcher.group.length
    1.57 -        }
    1.58 -        else 1
    1.59 -      val s = text.subSequence(i, i + len)
    1.60 -      i += len
    1.61 -      s.toString
    1.62 +      val n = matcher(i, text.length)
    1.63 +      val s = text.subSequence(i, i + n)
    1.64 +      i += n
    1.65 +      s
    1.66      }
    1.67    }
    1.68  
    1.69 @@ -71,20 +79,15 @@
    1.70      case class Entry(chr: Int, sym: Int)
    1.71      val index: Array[Entry] =
    1.72      {
    1.73 -      val matcher = regex.pattern.matcher(text)
    1.74 +      val matcher = new Matcher(text)
    1.75        val buf = new mutable.ArrayBuffer[Entry]
    1.76        var chr = 0
    1.77        var sym = 0
    1.78        while (chr < text.length) {
    1.79 -        val len =
    1.80 -          if (could_open(text.charAt(chr))) {
    1.81 -            matcher.region(chr, text.length).lookingAt
    1.82 -            matcher.group.length
    1.83 -          }
    1.84 -          else 1
    1.85 -        chr += len
    1.86 +        val n = matcher(chr, text.length)
    1.87 +        chr += n
    1.88          sym += 1
    1.89 -        if (len > 1) buf += Entry(chr, sym)
    1.90 +        if (n > 1) buf += Entry(chr, sym)
    1.91        }
    1.92        buf.toArray
    1.93      }
    1.94 @@ -153,7 +156,7 @@
    1.95  
    1.96    /** Symbol interpretation **/
    1.97  
    1.98 -  class Interpretation(symbol_decls: Iterator[String])
    1.99 +  class Interpretation(symbol_decls: List[String])
   1.100    {
   1.101      /* read symbols */
   1.102  
   1.103 @@ -180,7 +183,7 @@
   1.104      }
   1.105  
   1.106      private val symbols: List[(String, Map[String, String])] =
   1.107 -      for (decl <- symbol_decls.toList if !empty.pattern.matcher(decl).matches)
   1.108 +      for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
   1.109          yield read_decl(decl)
   1.110  
   1.111