mark hard tabs as single chunks, as required by jEdit;
authorwenzelm
Sun Sep 04 17:21:11 2011 +0200 (2011-09-04)
changeset 447010fd2bf8eaa9f
parent 44700 f4b42f310f86
child 44702 eb00752507c7
mark hard tabs as single chunks, as required by jEdit;
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Sep 04 16:37:22 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Sep 04 17:21:11 2011 +0200
     1.3 @@ -186,7 +186,8 @@
     1.4              val style = Isabelle_Markup.token_markup(syntax, token)
     1.5              val length = token.source.length
     1.6              val end_offset = offset + length
     1.7 -            if ((offset until end_offset) exists extended.isDefinedAt) {
     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 style1 =
    1.12                    extended.get(i) match {