tuned;
authorwenzelm
Mon Dec 04 16:28:06 2017 +0100 (4 months ago)
changeset 67126143f0ba01415
parent 67125 361b3ef643a7
child 67127 cf111622c9f8
tuned;
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/token_markup.scala	Mon Dec 04 16:28:00 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Mon Dec 04 16:28:06 2017 +0100
     1.3 @@ -271,10 +271,9 @@
     1.4          var offset = 0
     1.5          for ((style, token) <- styled_tokens) {
     1.6            val length = token.length
     1.7 -          val end_offset = offset + length
     1.8 -          if ((offset until end_offset) exists
     1.9 -              (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
    1.10 -            for (i <- offset until end_offset) {
    1.11 +          val offsets = offset until (offset + length)
    1.12 +          if (offsets.exists(i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
    1.13 +            for (i <- offsets) {
    1.14                val style1 =
    1.15                  extended.get(i) match {
    1.16                    case None => style