mark hard tabs as single chunks, as required by jEdit (see 0fd2bf8eaa9f);
authorwenzelm
Sat, 04 Oct 2014 18:26:25 +0200
changeset 58537 207fb06aa189
parent 58536 402a8e8107a7
child 58538 299b82d12d53
mark hard tabs as single chunks, as required by jEdit (see 0fd2bf8eaa9f);
src/Tools/jEdit/src/bibtex_token_markup.scala
--- a/src/Tools/jEdit/src/bibtex_token_markup.scala	Sat Oct 04 18:16:24 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_token_markup.scala	Sat Oct 04 18:26:25 2014 +0200
@@ -81,7 +81,13 @@
         for ((style, token) <- styled_tokens) {
           val length = token.length
           val end_offset = offset + length
-          handler.handleToken(line, style, offset, length, context1)
+
+          if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
+            for (i <- offset until end_offset)
+              handler.handleToken(line, style, i, 1, context1)
+          }
+          else handler.handleToken(line, style, offset, length, context1)
+
           offset += length
         }
         handler.handleToken(line, JEditToken.END, line.count, 0, context1)