1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 21:41:00 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 11:41:49 2011 +0200
     1.3 @@ -396,6 +396,7 @@
     1.4      painter.addMouseMotionListener(mouse_motion_listener)
     1.5      text_area.addCaretListener(caret_listener)
     1.6      text_area.addLeftOfScrollBar(overview)
     1.7 +    if (text_area.isCaretBlinkEnabled) text_area.setCaretBlinkEnabled(false)
     1.8      session.commands_changed += main_actor
     1.9      session.global_settings += main_actor
    1.10    }
    1.11 @@ -405,6 +406,7 @@
    1.12      val painter = text_area.getPainter
    1.13      session.commands_changed -= main_actor
    1.14      session.global_settings -= main_actor
    1.15 +		text_area.setCaretBlinkEnabled(jEdit.getBooleanProperty("view.caretBlink"))
    1.16      text_area.removeFocusListener(focus_listener)
    1.17      text_area.getView.removeWindowListener(window_listener)
    1.18      painter.removeMouseMotionListener(mouse_motion_listener)

     2.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Tue Jun 14 21:41:00 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 11:41:49 2011 +0200
     2.3 @@ -10,11 +10,13 @@
     2.4  import isabelle._
     2.5  
     2.6  import java.awt.Graphics2D
     2.7 +import java.awt.font.TextAttribute
     2.8 +import java.text.AttributedString
     2.9  import java.util.ArrayList
    2.10  
    2.11  import org.gjt.sp.jedit.Debug
    2.12  import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    2.13 -import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
    2.14 +import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, JEditTextArea}
    2.15  
    2.16  
    2.17  class Text_Area_Painter(doc_view: Document_View)
    2.18 @@ -23,9 +25,11 @@
    2.19    private val buffer = model.buffer
    2.20    private val text_area = doc_view.text_area
    2.21  
    2.22 -  private val orig_text_painter: TextAreaExtension =
    2.23 +
    2.24 +  /* original painters */
    2.25 +
    2.26 +  private def pick_extension(name: String): TextAreaExtension =
    2.27    {
    2.28 -    val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
    2.29      text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
    2.30      match {
    2.31        case List(x) => x
    2.32 @@ -33,6 +37,12 @@
    2.33      }
    2.34    }
    2.35  
    2.36 +  private val orig_text_painter =
    2.37 +    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
    2.38 +
    2.39 +  private val orig_caret_painter =
    2.40 +    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintCaret")
    2.41 +
    2.42  
    2.43    /* painter snapshot */
    2.44  
    2.45 @@ -183,10 +193,11 @@
    2.46    }
    2.47  
    2.48    private def paint_chunk_list(gfx: Graphics2D,
    2.49 -    offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
    2.50 +    offset: Text.Offset, caret_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
    2.51    {
    2.52      val clip_rect = gfx.getClipBounds
    2.53 -    val font_context = text_area.getPainter.getFontRenderContext
    2.54 +    val painter = text_area.getPainter
    2.55 +    val font_context = painter.getFontRenderContext
    2.56  
    2.57      var w = 0.0f
    2.58      var chunk_offset = offset
    2.59 @@ -206,7 +217,8 @@
    2.60  
    2.61          gfx.setFont(chunk_font)
    2.62          if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
    2.63 -            markup.forall(info => info.info.isEmpty)) {
    2.64 +            markup.forall(info => info.info.isEmpty) &&
    2.65 +            !chunk_range.contains(caret_offset)) {
    2.66            gfx.setColor(chunk_color)
    2.67            gfx.drawGlyphVector(chunk.gv, x + w, y)
    2.68          }
    2.69 @@ -215,7 +227,17 @@
    2.70            for (Text.Info(range, info) <- markup) {
    2.71              val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    2.72              gfx.setColor(info.getOrElse(chunk_color))
    2.73 -            gfx.drawString(str, x1.toInt, y.toInt)
    2.74 +            if (range.contains(caret_offset)) {
    2.75 +              val astr = new AttributedString(str)
    2.76 +              val i = caret_offset - range.start
    2.77 +              astr.addAttribute(TextAttribute.FONT, chunk_font)
    2.78 +              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, i + 1)
    2.79 +              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, i + 1)
    2.80 +              gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
    2.81 +            }
    2.82 +            else {
    2.83 +              gfx.drawString(str, x1.toInt, y.toInt)
    2.84 +            }
    2.85              x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    2.86            }
    2.87          }
    2.88 @@ -239,18 +261,27 @@
    2.89          val fm = text_area.getPainter.getFontMetrics
    2.90          var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
    2.91  
    2.92 +        val caret_offset =
    2.93 +          if (text_area.hasFocus) text_area.getCaretPosition
    2.94 +          else -1
    2.95 +
    2.96          val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
    2.97          for (i <- 0 until physical_lines.length) {
    2.98            if (physical_lines(i) != -1) {
    2.99 -            infos.get(start(i)) match {
   2.100 -              case Some(chunk) =>
   2.101 -                val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt
   2.102 -                gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   2.103 -                orig_text_painter.paintValidLine(gfx,
   2.104 -                  first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   2.105 -                gfx.setClip(clip)
   2.106 -              case None =>
   2.107 -            }
   2.108 +            val x1 =
   2.109 +              infos.get(start(i)) match {
   2.110 +                case None => x0
   2.111 +                case Some(chunk) =>
   2.112 +                  gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
   2.113 +                  val w = paint_chunk_list(gfx, start(i), caret_offset, chunk, x0, y0).toInt
   2.114 +                  x0 + w.toInt
   2.115 +              }
   2.116 +            gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   2.117 +            orig_text_painter.paintValidLine(gfx,
   2.118 +              first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   2.119 +            orig_caret_painter.paintValidLine(gfx,
   2.120 +              first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   2.121 +            gfx.setClip(clip)
   2.122            }
   2.123            y0 += line_height
   2.124          }
   2.125 @@ -269,11 +300,16 @@
   2.126      painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   2.127      painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
   2.128      painter.removeExtension(orig_text_painter)
   2.129 +    painter.removeExtension(orig_caret_painter)
   2.130    }
   2.131  
   2.132    def deactivate()
   2.133    {
   2.134      val painter = text_area.getPainter
   2.135 +    val caret_layer =
   2.136 +      if (painter.isBlockCaretEnabled) TextAreaPainter.BLOCK_CARET_LAYER
   2.137 +      else TextAreaPainter.CARET_LAYER
   2.138 +    painter.addExtension(caret_layer, orig_caret_painter)
   2.139      painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   2.140      painter.removeExtension(reset_snapshot)
   2.141      painter.removeExtension(text_painter)