1.1 --- a/src/Pure/General/symbol.scala	Fri Jul 03 21:14:46 2009 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Sat Jul 04 11:46:51 2009 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  package isabelle
     1.5  
     1.6  import scala.io.Source
     1.7 -import scala.collection.jcl
     1.8 +import scala.collection.{jcl, mutable}
     1.9  import scala.util.matching.Regex
    1.10  
    1.11  
    1.12 @@ -34,14 +34,59 @@
    1.13    def is_open(s: String): Boolean =
    1.14    {
    1.15      val len = s.length
    1.16 -    len == 1 && Character.isHighSurrogate(s(0)) ||
    1.17 +    len == 1 && Character.isLowSurrogate(s(0)) ||
    1.18      s == "\\" ||
    1.19      s == "\\<" ||
    1.20      len > 2 && s(len - 1) != '>'
    1.21    }
    1.22  
    1.23  
    1.24 -  /** Recoding **/
    1.25 +  /** Decoding offsets **/
    1.26 +
    1.27 +  class Index(text: String)
    1.28 +  {
    1.29 +    case class Entry(chr: Int, sym: Int)
    1.30 +    val index: Array[Entry] =
    1.31 +    {
    1.32 +      val length = text.length
    1.33 +      val matcher = regex.pattern.matcher(text)
    1.34 +      val buf = new mutable.ArrayBuffer[Entry]
    1.35 +      var chr = 0
    1.36 +      var sym = 0
    1.37 +      while (chr < length) {
    1.38 +        val c = text(chr)
    1.39 +        val len =
    1.40 +          if (c == '\\' || Character.isHighSurrogate(c)) {
    1.41 +            matcher.region(chr, length).lookingAt
    1.42 +            matcher.group.length
    1.43 +          } else 1
    1.44 +        chr += len
    1.45 +        sym += 1
    1.46 +        if (len > 1) buf += Entry(chr, sym)
    1.47 +      }
    1.48 +      buf.toArray
    1.49 +    }
    1.50 +    def decode(sym: Int): Int =
    1.51 +    {
    1.52 +      val end = index.length
    1.53 +      def bisect(a: Int, b: Int): Int =
    1.54 +      {
    1.55 +        if (a < b) {
    1.56 +          val c = (a + b) / 2
    1.57 +          if (sym < index(c).sym) bisect(a, c)
    1.58 +          else if (c + 1 == end || sym < index(c + 1).sym) c
    1.59 +          else bisect(c + 1, b)
    1.60 +        }
    1.61 +        else -1
    1.62 +      }
    1.63 +      val i = bisect(0, end)
    1.64 +      if (i < 0) sym
    1.65 +      else index(i).chr + sym - index(i).sym
    1.66 +    }
    1.67 +  }
    1.68 +
    1.69 +
    1.70 +  /** Recoding text **/
    1.71  
    1.72    private class Recoder(list: List[(String, String)])
    1.73    {
    1.74 @@ -71,8 +116,7 @@
    1.75        while (i < len) {
    1.76          val c = text(i)
    1.77          if (min <= c && c <= max) {
    1.78 -          matcher.region(i, len)
    1.79 -          matcher.lookingAt
    1.80 +          matcher.region(i, len).lookingAt
    1.81            val x = matcher.group
    1.82            result.append(table.get(x) getOrElse x)
    1.83            i = matcher.end