src/Tools/jEdit/src/text_area_painter.scala
changeset 43426 24e2e2f0032b
parent 43419 6ed49c52d463
child 43428 b41dea5772c6
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Fri Jun 17 23:18:22 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Fri Jun 17 23:20:34 2011 +0200
     1.3 @@ -219,7 +219,9 @@
     1.4          val chunk_font = chunk.style.getFont
     1.5          val chunk_color = chunk.style.getForegroundColor
     1.6  
     1.7 -        val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
     1.8 +        val markup =
     1.9 +          painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
    1.10 +            .map(_.restrict(chunk_range))
    1.11  
    1.12          gfx.setFont(chunk_font)
    1.13          if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
    1.14 @@ -228,14 +230,17 @@
    1.15            gfx.setColor(chunk_color)
    1.16            gfx.drawGlyphVector(chunk.gv, x + w, y)
    1.17          }
    1.18 -        else {
    1.19 +        else if (!markup.isEmpty) {
    1.20            var x1 = x + w
    1.21 -          for (Text.Info(range, info) <- markup) {
    1.22 -            // FIXME proper range!?
    1.23 -            val str =
    1.24 -              chunk.str.substring(
    1.25 -                (range.start - chunk_offset) max 0,
    1.26 -                (range.stop - chunk_offset) min chunk_length)
    1.27 +          for {
    1.28 +            Text.Info(r, info) <-
    1.29 +              Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
    1.30 +              markup.iterator ++
    1.31 +              Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
    1.32 +            val range = r.restrict(chunk_range)
    1.33 +            if !range.is_singularity
    1.34 +          } {
    1.35 +            val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    1.36              gfx.setColor(info.getOrElse(chunk_color))
    1.37              if (range.contains(caret_offset)) {
    1.38                val astr = new AttributedString(str)