tuned iteration over short symbols;
authorwenzelm
Tue Jun 21 13:29:44 2011 +0200 (2011-06-21 ago)
changeset 43489132f99cc0a43
parent 43488 39035276927c
child 43490 5e6f76cacb93
tuned iteration over short symbols;
src/Pure/General/symbol.scala
src/Pure/Thy/html.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/General/symbol.scala	Tue Jun 21 12:53:55 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Tue Jun 21 13:29:44 2011 +0200
     1.3 @@ -85,21 +85,38 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* iterator */
     1.8 +  /* efficient iterators */
     1.9  
    1.10 -  def iterator(text: CharSequence) = new Iterator[CharSequence]
    1.11 -  {
    1.12 -    private val matcher = new Matcher(text)
    1.13 -    private var i = 0
    1.14 -    def hasNext = i < text.length
    1.15 -    def next =
    1.16 +  def iterator(text: CharSequence): Iterator[CharSequence] =
    1.17 +    new Iterator[CharSequence]
    1.18      {
    1.19 -      val n = matcher(i, text.length)
    1.20 -      val s = text.subSequence(i, i + n)
    1.21 -      i += n
    1.22 -      s
    1.23 +      private val matcher = new Matcher(text)
    1.24 +      private var i = 0
    1.25 +      def hasNext = i < text.length
    1.26 +      def next =
    1.27 +      {
    1.28 +        val n = matcher(i, text.length)
    1.29 +        val s = text.subSequence(i, i + n)
    1.30 +        i += n
    1.31 +        s
    1.32 +      }
    1.33      }
    1.34 -  }
    1.35 +
    1.36 +  private val char_symbols: Array[String] =
    1.37 +    (0 to 127).iterator.map(i => new String(Array(i.toChar))).toArray
    1.38 +
    1.39 +  private def make_string(sym: CharSequence): String =
    1.40 +    sym.length match {
    1.41 +      case 0 => ""
    1.42 +      case 1 =>
    1.43 +        val c = sym.charAt(0)
    1.44 +        if (c < char_symbols.length) char_symbols(c)
    1.45 +        else sym.toString
    1.46 +      case _ => sym.toString
    1.47 +    }
    1.48 +
    1.49 +  def iterator_string(text: CharSequence): Iterator[String] =
    1.50 +    iterator(text).map(make_string)
    1.51  
    1.52  
    1.53    /* decoding offsets */
     2.1 --- a/src/Pure/Thy/html.scala	Tue Jun 21 12:53:55 2011 +0200
     2.2 +++ b/src/Pure/Thy/html.scala	Tue Jun 21 13:29:44 2011 +0200
     2.3 @@ -73,7 +73,7 @@
     2.4              flush()
     2.5              ts += elem
     2.6            }
     2.7 -          val syms = Symbol.iterator(txt).map(_.toString)
     2.8 +          val syms = Symbol.iterator_string(txt)
     2.9            while (syms.hasNext) {
    2.10              val s1 = syms.next
    2.11              def s2() = if (syms.hasNext) syms.next else ""
     3.1 --- a/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 12:53:55 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 13:29:44 2011 +0200
     3.3 @@ -90,7 +90,7 @@
     3.4      }
     3.5      var offset = 0
     3.6      var ctrl = ""
     3.7 -    for (sym <- Symbol.iterator(text).map(_.toString)) {
     3.8 +    for (sym <- Symbol.iterator_string(text)) {
     3.9        if (ctrl_style(sym).isDefined) ctrl = sym
    3.10        else if (ctrl != "") {
    3.11          if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {