# HG changeset patch
# User wenzelm
# Date 1315149671 -7200
# Node ID 0fd2bf8eaa9ff631628695b8b5e76ee82bca2b10
# Parent  f4b42f310f86c0d28f8a99a678effb998796faea
mark hard tabs as single chunks, as required by jEdit;

diff -r f4b42f310f86 -r 0fd2bf8eaa9f src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sun Sep 04 16:37:22 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sun Sep 04 17:21:11 2011 +0200
@@ -186,7 +186,8 @@
             val style = Isabelle_Markup.token_markup(syntax, token)
             val length = token.source.length
             val end_offset = offset + length
-            if ((offset until end_offset) exists extended.isDefinedAt) {
+            if ((offset until end_offset) exists
+                (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
               for (i <- offset until end_offset) {
                 val style1 =
                   extended.get(i) match {