1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 18:57:38 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 21:03:52 2011 +0200
     1.3 @@ -186,8 +186,8 @@
     1.4      result
     1.5    }
     1.6  
     1.7 -  private def paint_chunk_list(gfx: Graphics2D,
     1.8 -    offset: Text.Offset, caret_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
     1.9 +  private def paint_chunk_list(
    1.10 +    gfx: Graphics2D, offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
    1.11    {
    1.12      val clip_rect = gfx.getClipBounds
    1.13      val painter = text_area.getPainter
    1.14 @@ -207,6 +207,10 @@
    1.15          val chunk_font = chunk.style.getFont
    1.16          val chunk_color = chunk.style.getForegroundColor
    1.17  
    1.18 +        val caret_range =
    1.19 +          if (text_area.hasFocus) doc_view.caret_range()
    1.20 +          else Text.Range(-1)
    1.21 +
    1.22          val markup =
    1.23            for {
    1.24              x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
    1.25 @@ -214,13 +218,9 @@
    1.26            } yield y
    1.27  
    1.28          gfx.setFont(chunk_font)
    1.29 -        if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
    1.30 -            markup.forall(info => info.info.isEmpty) &&
    1.31 -            !chunk_range.contains(caret_offset)) {
    1.32 -          gfx.setColor(chunk_color)
    1.33 -          gfx.drawGlyphVector(chunk.gv, x + w, y)
    1.34 -        }
    1.35 -        else if (!markup.isEmpty) {
    1.36 +        if (markup.isEmpty)
    1.37 +          gfx.drawString(chunk.str, x.toInt, y.toInt)
    1.38 +        else {
    1.39            var x1 = x + w
    1.40            for {
    1.41              Text.Info(range, info) <-
    1.42 @@ -231,16 +231,18 @@
    1.43            } {
    1.44              val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    1.45              gfx.setColor(info.getOrElse(chunk_color))
    1.46 -            if (range.contains(caret_offset)) {
    1.47 -              val astr = new AttributedString(str)
    1.48 -              val i = caret_offset - range.start
    1.49 -              astr.addAttribute(TextAttribute.FONT, chunk_font)
    1.50 -              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, i + 1)
    1.51 -              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, i + 1)
    1.52 -              gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
    1.53 -            }
    1.54 -            else {
    1.55 -              gfx.drawString(str, x1.toInt, y.toInt)
    1.56 +
    1.57 +            range.try_restrict(caret_range) match {
    1.58 +              case Some(r) if !r.is_singularity =>
    1.59 +                val astr = new AttributedString(str)
    1.60 +                val i = r.start - range.start
    1.61 +                val j = r.stop - range.start
    1.62 +                astr.addAttribute(TextAttribute.FONT, chunk_font)
    1.63 +                astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
    1.64 +                astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
    1.65 +                gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
    1.66 +              case _ =>
    1.67 +                gfx.drawString(str, x1.toInt, y.toInt)
    1.68              }
    1.69              x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    1.70            }
    1.71 @@ -265,10 +267,6 @@
    1.72          val fm = text_area.getPainter.getFontMetrics
    1.73          var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
    1.74  
    1.75 -        val caret_offset =
    1.76 -          if (text_area.hasFocus) text_area.getCaretPosition
    1.77 -          else -1
    1.78 -
    1.79          val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
    1.80          for (i <- 0 until physical_lines.length) {
    1.81            if (physical_lines(i) != -1) {
    1.82 @@ -277,7 +275,7 @@
    1.83                  case None => x0
    1.84                  case Some(chunk) =>
    1.85                    gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
    1.86 -                  val w = paint_chunk_list(gfx, start(i), caret_offset, chunk, x0, y0).toInt
    1.87 +                  val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt
    1.88                    x0 + w.toInt
    1.89                }
    1.90              gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)