# HG changeset patch
# User wenzelm
# Date 1512401286 -3600
# Node ID 143f0ba0141530c9fc086cd078841972ab828002
# Parent  361b3ef643a786ed3f93d48856a4c16208196229
tuned;

diff -r 361b3ef643a7 -r 143f0ba01415 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Mon Dec 04 16:28:00 2017 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Mon Dec 04 16:28:06 2017 +0100
@@ -271,10 +271,9 @@
         var offset = 0
         for ((style, token) <- styled_tokens) {
           val length = token.length
-          val end_offset = offset + length
-          if ((offset until end_offset) exists
-              (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
-            for (i <- offset until end_offset) {
+          val offsets = offset until (offset + length)
+          if (offsets.exists(i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
+            for (i <- offsets) {
               val style1 =
                 extended.get(i) match {
                   case None => style