src/Tools/jEdit/src/rich_text_area.scala
author wenzelm
Tue Feb 25 20:15:47 2014 +0100 (2014-02-25)
changeset 55747 bef19c929ba5
parent 55726 945ad7eaf37f
child 55766 6a16443e520e
permissions -rw-r--r--
more completion rendering: active, semantic, syntactic;
tuned;
wenzelm@49411
     1
/*  Title:      Tools/jEdit/src/rich_text_area.scala
wenzelm@43369
     2
    Author:     Makarius
wenzelm@43369
     3
wenzelm@49411
     4
Enhanced version of jEdit text area, with rich text rendering,
wenzelm@49411
     5
tooltips, hyperlinks etc.
wenzelm@43369
     6
*/
wenzelm@43369
     7
wenzelm@43369
     8
package isabelle.jedit
wenzelm@43369
     9
wenzelm@43369
    10
wenzelm@43369
    11
import isabelle._
wenzelm@43369
    12
wenzelm@50657
    13
import java.awt.{Graphics2D, Shape, Color, Point, Toolkit}
wenzelm@49410
    14
import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
wenzelm@49410
    15
  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
wenzelm@43392
    16
import java.awt.font.TextAttribute
wenzelm@43392
    17
import java.text.AttributedString
wenzelm@43369
    18
import java.util.ArrayList
wenzelm@43369
    19
wenzelm@49410
    20
import org.gjt.sp.util.Log
wenzelm@49410
    21
import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
wenzelm@43369
    22
import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
wenzelm@49410
    23
import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
wenzelm@49410
    24
wenzelm@49410
    25
wenzelm@49492
    26
class Rich_Text_Area(
wenzelm@49492
    27
  view: View,
wenzelm@49492
    28
  text_area: TextArea,
wenzelm@50199
    29
  get_rendering: () => Rendering,
wenzelm@50915
    30
  close_action: () => Unit,
wenzelm@50306
    31
  caret_visible: Boolean,
wenzelm@53179
    32
  enable_hovering: Boolean)
wenzelm@49410
    33
{
wenzelm@49410
    34
  private val buffer = text_area.getBuffer
wenzelm@43369
    35
wenzelm@43369
    36
wenzelm@49410
    37
  /* robust extension body */
wenzelm@49410
    38
wenzelm@49410
    39
  def robust_body[A](default: A)(body: => A): A =
wenzelm@49410
    40
  {
wenzelm@49410
    41
    try {
wenzelm@49410
    42
      Swing_Thread.require()
wenzelm@49410
    43
      if (buffer == text_area.getBuffer) body
wenzelm@49410
    44
      else {
wenzelm@49410
    45
        Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
wenzelm@49410
    46
        default
wenzelm@49410
    47
      }
wenzelm@49410
    48
    }
wenzelm@50641
    49
    catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default }
wenzelm@49410
    50
  }
wenzelm@43376
    51
wenzelm@43392
    52
wenzelm@43392
    53
  /* original painters */
wenzelm@43392
    54
wenzelm@43392
    55
  private def pick_extension(name: String): TextAreaExtension =
wenzelm@43369
    56
  {
wenzelm@43369
    57
    text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
wenzelm@43369
    58
    match {
wenzelm@43369
    59
      case List(x) => x
wenzelm@43369
    60
      case _ => error("Expected exactly one " + name)
wenzelm@43369
    61
    }
wenzelm@43369
    62
  }
wenzelm@43369
    63
wenzelm@43392
    64
  private val orig_text_painter =
wenzelm@43392
    65
    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
wenzelm@43392
    66
wenzelm@43392
    67
wenzelm@43393
    68
  /* common painter state */
wenzelm@43381
    69
wenzelm@50199
    70
  @volatile private var painter_rendering: Rendering = null
wenzelm@43393
    71
  @volatile private var painter_clip: Shape = null
wenzelm@43381
    72
wenzelm@43393
    73
  private val set_state = new TextAreaExtension
wenzelm@43381
    74
  {
wenzelm@43381
    75
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
    76
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
    77
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
    78
    {
wenzelm@49410
    79
      painter_rendering = get_rendering()
wenzelm@46220
    80
      painter_clip = gfx.getClip
wenzelm@43381
    81
    }
wenzelm@43381
    82
  }
wenzelm@43381
    83
wenzelm@43393
    84
  private val reset_state = new TextAreaExtension
wenzelm@43369
    85
  {
wenzelm@43381
    86
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
    87
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
    88
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
    89
    {
wenzelm@49356
    90
      painter_rendering = null
wenzelm@46220
    91
      painter_clip = null
wenzelm@43381
    92
    }
wenzelm@43381
    93
  }
wenzelm@43381
    94
wenzelm@50199
    95
  def robust_rendering(body: Rendering => Unit)
wenzelm@46220
    96
  {
wenzelm@49410
    97
    robust_body(()) { body(painter_rendering) }
wenzelm@49410
    98
  }
wenzelm@49410
    99
wenzelm@49410
   100
wenzelm@49410
   101
  /* active areas within the text */
wenzelm@49410
   102
wenzelm@50199
   103
  private class Active_Area[A](rendering: Rendering => Text.Range => Option[Text.Info[A]])
wenzelm@49410
   104
  {
wenzelm@49493
   105
    private var the_text_info: Option[(String, Text.Info[A])] = None
wenzelm@49410
   106
wenzelm@55688
   107
    def is_active: Boolean = the_text_info.isDefined
wenzelm@49493
   108
    def text_info: Option[(String, Text.Info[A])] = the_text_info
wenzelm@49493
   109
    def info: Option[Text.Info[A]] = the_text_info.map(_._2)
wenzelm@49410
   110
wenzelm@49410
   111
    def update(new_info: Option[Text.Info[A]])
wenzelm@49410
   112
    {
wenzelm@49493
   113
      val old_text_info = the_text_info
wenzelm@49493
   114
      val new_text_info =
wenzelm@49493
   115
        new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
wenzelm@49493
   116
wenzelm@49493
   117
      if (new_text_info != old_text_info) {
wenzelm@49493
   118
        for {
wenzelm@49493
   119
          r0 <- JEdit_Lib.visible_range(text_area)
wenzelm@49493
   120
          opt <- List(old_text_info, new_text_info)
wenzelm@49493
   121
          (_, Text.Info(r1, _)) <- opt
wenzelm@49493
   122
          r2 <- r1.try_restrict(r0)  // FIXME more precise?!
wenzelm@49493
   123
        } JEdit_Lib.invalidate_range(text_area, r2)
wenzelm@49493
   124
        the_text_info = new_text_info
wenzelm@49410
   125
      }
wenzelm@49410
   126
    }
wenzelm@49410
   127
wenzelm@50199
   128
    def update_rendering(r: Rendering, range: Text.Range)
wenzelm@49410
   129
    { update(rendering(r)(range)) }
wenzelm@49410
   130
wenzelm@49410
   131
    def reset { update(None) }
wenzelm@49410
   132
  }
wenzelm@49410
   133
wenzelm@49410
   134
  // owned by Swing thread
wenzelm@49410
   135
wenzelm@50199
   136
  private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
wenzelm@52980
   137
  private val hyperlink_area =
wenzelm@52980
   138
    new Active_Area[PIDE.editor.Hyperlink]((r: Rendering) => r.hyperlink _)
wenzelm@50450
   139
  private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _)
wenzelm@49492
   140
wenzelm@49492
   141
  private val active_areas =
wenzelm@50450
   142
    List((highlight_area, true), (hyperlink_area, true), (active_area, false))
wenzelm@50216
   143
  def active_reset(): Unit = active_areas.foreach(_._1.reset)
wenzelm@49410
   144
wenzelm@49410
   145
  private val focus_listener = new FocusAdapter {
wenzelm@49424
   146
    override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
wenzelm@49410
   147
  }
wenzelm@49410
   148
wenzelm@49410
   149
  private val window_listener = new WindowAdapter {
wenzelm@49424
   150
    override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } }
wenzelm@49424
   151
    override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } }
wenzelm@49410
   152
  }
wenzelm@49410
   153
wenzelm@49410
   154
  private val mouse_listener = new MouseAdapter {
wenzelm@49410
   155
    override def mouseClicked(e: MouseEvent) {
wenzelm@49424
   156
      robust_body(()) {
wenzelm@49424
   157
        hyperlink_area.info match {
wenzelm@52482
   158
          case Some(Text.Info(_, link)) =>
wenzelm@52482
   159
            link.follow(view)
wenzelm@49492
   160
          case None =>
wenzelm@49492
   161
        }
wenzelm@50450
   162
        active_area.text_info match {
wenzelm@50915
   163
          case Some((text, Text.Info(_, markup))) =>
wenzelm@50915
   164
            Active.action(view, text, markup)
wenzelm@50915
   165
            close_action()
wenzelm@49424
   166
          case None =>
wenzelm@49424
   167
        }
wenzelm@49410
   168
      }
wenzelm@49410
   169
    }
wenzelm@49410
   170
  }
wenzelm@49410
   171
wenzelm@49410
   172
  private val mouse_motion_listener = new MouseMotionAdapter {
wenzelm@53182
   173
    override def mouseMoved(evt: MouseEvent) {
wenzelm@49424
   174
      robust_body(()) {
wenzelm@53182
   175
        val x = evt.getX
wenzelm@53182
   176
        val y = evt.getY
wenzelm@53182
   177
        val control = (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
wenzelm@49492
   178
wenzelm@53179
   179
        if ((control || enable_hovering) && !buffer.isLoading) {
wenzelm@49424
   180
          JEdit_Lib.buffer_lock(buffer) {
wenzelm@53182
   181
            JEdit_Lib.pixel_range(text_area, x, y) match {
wenzelm@50211
   182
              case None => active_reset()
wenzelm@49941
   183
              case Some(range) =>
wenzelm@49941
   184
                val rendering = get_rendering()
wenzelm@49941
   185
                for ((area, require_control) <- active_areas)
wenzelm@49941
   186
                {
wenzelm@50165
   187
                  if (control == require_control && !rendering.snapshot.is_outdated)
wenzelm@49941
   188
                    area.update_rendering(rendering, range)
wenzelm@49941
   189
                  else area.reset
wenzelm@49941
   190
                }
wenzelm@49492
   191
            }
wenzelm@49424
   192
          }
wenzelm@49410
   193
        }
wenzelm@49424
   194
        else active_reset()
wenzelm@51441
   195
wenzelm@53182
   196
        if (evt.getSource == text_area.getPainter) {
wenzelm@52494
   197
          Pretty_Tooltip.invoke(() =>
wenzelm@52495
   198
            robust_body(()) {
wenzelm@52494
   199
              val rendering = get_rendering()
wenzelm@52494
   200
              val snapshot = rendering.snapshot
wenzelm@52494
   201
              if (!snapshot.is_outdated) {
wenzelm@52494
   202
                JEdit_Lib.pixel_range(text_area, x, y) match {
wenzelm@52494
   203
                  case None =>
wenzelm@52494
   204
                  case Some(range) =>
wenzelm@52494
   205
                    val result =
wenzelm@52494
   206
                      if (control) rendering.tooltip(range)
wenzelm@52494
   207
                      else rendering.tooltip_message(range)
wenzelm@52494
   208
                    result match {
wenzelm@52494
   209
                      case None =>
wenzelm@52494
   210
                      case Some(tip) =>
wenzelm@52494
   211
                        val painter = text_area.getPainter
wenzelm@53247
   212
                        val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
wenzelm@52494
   213
                        val results = rendering.command_results(range)
wenzelm@53247
   214
                        Pretty_Tooltip(view, painter, loc, rendering, results, tip)
wenzelm@52494
   215
                    }
wenzelm@52494
   216
                }
wenzelm@52494
   217
              }
wenzelm@52495
   218
          })
wenzelm@51452
   219
        }
wenzelm@49410
   220
      }
wenzelm@49410
   221
    }
wenzelm@49410
   222
  }
wenzelm@49410
   223
wenzelm@49410
   224
wenzelm@55713
   225
  /* text background */
wenzelm@55713
   226
wenzelm@43381
   227
  private val background_painter = new TextAreaExtension
wenzelm@43381
   228
  {
wenzelm@43381
   229
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
   230
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
   231
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
   232
    {
wenzelm@49356
   233
      robust_rendering { rendering =>
wenzelm@51581
   234
        val fm = text_area.getPainter.getFontMetrics
wenzelm@43376
   235
wenzelm@43381
   236
        for (i <- 0 until physical_lines.length) {
wenzelm@43381
   237
          if (physical_lines(i) != -1) {
wenzelm@49843
   238
            val line_range = Text.Range(start(i), end(i))
wenzelm@43376
   239
wenzelm@49473
   240
            // line background color
wenzelm@49473
   241
            for { (color, separator) <- rendering.line_background(line_range) }
wenzelm@49473
   242
            {
wenzelm@49473
   243
              gfx.setColor(color)
wenzelm@49475
   244
              val sep = if (separator) (2 min (line_height / 2)) else 0
wenzelm@49475
   245
              gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
wenzelm@49473
   246
            }
wenzelm@49473
   247
wenzelm@46166
   248
            // background color (1)
wenzelm@43381
   249
            for {
wenzelm@49356
   250
              Text.Info(range, color) <- rendering.background1(line_range)
wenzelm@49409
   251
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@43381
   252
            } {
wenzelm@43381
   253
              gfx.setColor(color)
wenzelm@43381
   254
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@43381
   255
            }
wenzelm@43376
   256
wenzelm@50450
   257
            // active area -- potentially from other snapshot
wenzelm@49492
   258
            for {
wenzelm@50450
   259
              info <- active_area.info
wenzelm@49492
   260
              Text.Info(range, _) <- info.try_restrict(line_range)
wenzelm@49492
   261
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@49492
   262
            } {
wenzelm@50450
   263
              gfx.setColor(rendering.active_hover_color)
wenzelm@49492
   264
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@49492
   265
            }
wenzelm@49492
   266
wenzelm@46166
   267
            // background color (2)
wenzelm@43381
   268
            for {
wenzelm@49356
   269
              Text.Info(range, color) <- rendering.background2(line_range)
wenzelm@49409
   270
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@43381
   271
            } {
wenzelm@43381
   272
              gfx.setColor(color)
wenzelm@43381
   273
              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
wenzelm@43376
   274
            }
wenzelm@43381
   275
wenzelm@43381
   276
            // squiggly underline
wenzelm@43381
   277
            for {
wenzelm@49356
   278
              Text.Info(range, color) <- rendering.squiggly_underline(line_range)
wenzelm@49409
   279
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@43381
   280
            } {
wenzelm@43381
   281
              gfx.setColor(color)
wenzelm@43381
   282
              val x0 = (r.x / 2) * 2
wenzelm@51574
   283
              val y0 = r.y + fm.getAscent + 1
wenzelm@43381
   284
              for (x1 <- Range(x0, x0 + r.length, 2)) {
wenzelm@43381
   285
                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
wenzelm@43381
   286
                gfx.drawLine(x1, y1, x1 + 1, y1)
wenzelm@43376
   287
              }
wenzelm@43376
   288
            }
wenzelm@43376
   289
          }
wenzelm@43376
   290
        }
wenzelm@43376
   291
      }
wenzelm@43381
   292
    }
wenzelm@43381
   293
  }
wenzelm@43381
   294
wenzelm@43381
   295
wenzelm@43381
   296
  /* text */
wenzelm@43369
   297
wenzelm@55747
   298
  private def caret_color(rendering: Rendering): Color =
wenzelm@55747
   299
  {
wenzelm@55747
   300
    if (text_area.isCaretVisible)
wenzelm@55747
   301
      text_area.getPainter.getCaretColor
wenzelm@55747
   302
    else rendering.caret_invisible_color
wenzelm@55747
   303
  }
wenzelm@55747
   304
wenzelm@50199
   305
  private def paint_chunk_list(rendering: Rendering,
wenzelm@43505
   306
    gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
wenzelm@43382
   307
  {
wenzelm@43382
   308
    val clip_rect = gfx.getClipBounds
wenzelm@43392
   309
    val painter = text_area.getPainter
wenzelm@43392
   310
    val font_context = painter.getFontRenderContext
wenzelm@55747
   311
wenzelm@55747
   312
    val caret_range =
wenzelm@55747
   313
      if (caret_visible) JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
wenzelm@55747
   314
      else Text.Range(-1)
wenzelm@43382
   315
wenzelm@43382
   316
    var w = 0.0f
wenzelm@43382
   317
    var chunk = head
wenzelm@43382
   318
    while (chunk != null) {
wenzelm@43505
   319
      val chunk_offset = line_start + chunk.offset
wenzelm@43382
   320
      if (x + w + chunk.width > clip_rect.x &&
wenzelm@50306
   321
          x + w < clip_rect.x + clip_rect.width && chunk.length > 0)
wenzelm@43382
   322
      {
wenzelm@43505
   323
        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
wenzelm@44662
   324
        val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
wenzelm@43382
   325
        val chunk_font = chunk.style.getFont
wenzelm@43382
   326
        val chunk_color = chunk.style.getForegroundColor
wenzelm@43382
   327
wenzelm@44056
   328
        def string_width(s: String): Float =
wenzelm@44056
   329
          if (s.isEmpty) 0.0f
wenzelm@44056
   330
          else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
wenzelm@44056
   331
wenzelm@43426
   332
        val markup =
wenzelm@43428
   333
          for {
wenzelm@49356
   334
            r1 <- rendering.text_color(chunk_range, chunk_color)
wenzelm@43450
   335
            r2 <- r1.try_restrict(chunk_range)
wenzelm@43450
   336
          } yield r2
wenzelm@43382
   337
wenzelm@43759
   338
        val padded_markup =
wenzelm@43759
   339
          if (markup.isEmpty)
wenzelm@46197
   340
            Iterator(Text.Info(chunk_range, chunk_color))
wenzelm@43759
   341
          else
wenzelm@46197
   342
            Iterator(
wenzelm@46197
   343
              Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
wenzelm@43759
   344
            markup.iterator ++
wenzelm@46197
   345
            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
wenzelm@43759
   346
wenzelm@43450
   347
        var x1 = x + w
wenzelm@43382
   348
        gfx.setFont(chunk_font)
wenzelm@46197
   349
        for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
wenzelm@44662
   350
          val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
wenzelm@46197
   351
          gfx.setColor(color)
wenzelm@43448
   352
wenzelm@43759
   353
          range.try_restrict(caret_range) match {
wenzelm@43759
   354
            case Some(r) if !r.is_singularity =>
wenzelm@43759
   355
              val i = r.start - range.start
wenzelm@43759
   356
              val j = r.stop - range.start
wenzelm@44056
   357
              val s1 = str.substring(0, i)
wenzelm@44056
   358
              val s2 = str.substring(i, j)
wenzelm@44056
   359
              val s3 = str.substring(j)
wenzelm@44056
   360
wenzelm@44056
   361
              if (!s1.isEmpty) gfx.drawString(s1, x1, y)
wenzelm@44056
   362
wenzelm@44056
   363
              val astr = new AttributedString(s2)
wenzelm@43759
   364
              astr.addAttribute(TextAttribute.FONT, chunk_font)
wenzelm@55747
   365
              astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering))
wenzelm@44056
   366
              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
wenzelm@44056
   367
              gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
wenzelm@44056
   368
wenzelm@44056
   369
              if (!s3.isEmpty)
wenzelm@44056
   370
                gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
wenzelm@44056
   371
wenzelm@43759
   372
            case _ =>
wenzelm@43759
   373
              gfx.drawString(str, x1, y)
wenzelm@43382
   374
          }
wenzelm@44056
   375
          x1 += string_width(str)
wenzelm@43382
   376
        }
wenzelm@43382
   377
      }
wenzelm@43382
   378
      w += chunk.width
wenzelm@43382
   379
      chunk = chunk.next.asInstanceOf[Chunk]
wenzelm@43382
   380
    }
wenzelm@43382
   381
    w
wenzelm@43382
   382
  }
wenzelm@43382
   383
wenzelm@43381
   384
  private val text_painter = new TextAreaExtension
wenzelm@43381
   385
  {
wenzelm@43381
   386
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
   387
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43382
   388
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
   389
    {
wenzelm@49356
   390
      robust_rendering { rendering =>
wenzelm@51581
   391
        val painter = text_area.getPainter
wenzelm@51581
   392
        val fm = painter.getFontMetrics
wenzelm@51581
   393
        val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext)
wenzelm@51581
   394
wenzelm@43381
   395
        val clip = gfx.getClip
wenzelm@43381
   396
        val x0 = text_area.getHorizontalOffset
wenzelm@43382
   397
        var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
wenzelm@43372
   398
wenzelm@51581
   399
        val (bullet_x, bullet_y, bullet_w, bullet_h) =
wenzelm@51581
   400
        {
wenzelm@51581
   401
          val w = fm.charWidth(' ')
wenzelm@51581
   402
          val b = (w / 2) max 1
wenzelm@51581
   403
          val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt
wenzelm@51581
   404
          ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
wenzelm@51581
   405
        }
wenzelm@51581
   406
wenzelm@43381
   407
        for (i <- 0 until physical_lines.length) {
wenzelm@49097
   408
          val line = physical_lines(i)
wenzelm@49097
   409
          if (line != -1) {
wenzelm@51581
   410
            val line_range = Text.Range(start(i), end(i))
wenzelm@51581
   411
wenzelm@51581
   412
            // bullet bar
wenzelm@51581
   413
            for {
wenzelm@51581
   414
              Text.Info(range, color) <- rendering.bullet(line_range)
wenzelm@51581
   415
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@51581
   416
            } {
wenzelm@51581
   417
              gfx.setColor(color)
wenzelm@51581
   418
              gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
wenzelm@51581
   419
                r.length - bullet_w, line_height - bullet_h)
wenzelm@51581
   420
            }
wenzelm@51581
   421
wenzelm@51581
   422
            // text chunks
wenzelm@49097
   423
            val screen_line = first_line + i
wenzelm@49097
   424
            val chunks = text_area.getChunksOfScreenLine(screen_line)
wenzelm@49097
   425
            if (chunks != null) {
wenzelm@49410
   426
              val line_start = buffer.getLineStartOffset(line)
wenzelm@49097
   427
              gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
wenzelm@49356
   428
              val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
wenzelm@49097
   429
              gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
wenzelm@49097
   430
              orig_text_painter.paintValidLine(gfx,
wenzelm@49097
   431
                screen_line, line, start(i), end(i), y + line_height * i)
wenzelm@49097
   432
              gfx.setClip(clip)
wenzelm@49097
   433
            }
wenzelm@43369
   434
          }
wenzelm@43381
   435
          y0 += line_height
wenzelm@43369
   436
        }
wenzelm@43369
   437
      }
wenzelm@43369
   438
    }
wenzelm@43369
   439
  }
wenzelm@43369
   440
wenzelm@43369
   441
wenzelm@43435
   442
  /* foreground */
wenzelm@43435
   443
wenzelm@43435
   444
  private val foreground_painter = new TextAreaExtension
wenzelm@43435
   445
  {
wenzelm@43435
   446
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43435
   447
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43435
   448
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43435
   449
    {
wenzelm@49356
   450
      robust_rendering { rendering =>
wenzelm@43435
   451
        for (i <- 0 until physical_lines.length) {
wenzelm@43435
   452
          if (physical_lines(i) != -1) {
wenzelm@49843
   453
            val line_range = Text.Range(start(i), end(i))
wenzelm@43435
   454
wenzelm@44545
   455
            // foreground color
wenzelm@44545
   456
            for {
wenzelm@49356
   457
              Text.Info(range, color) <- rendering.foreground(line_range)
wenzelm@49409
   458
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@44545
   459
            } {
wenzelm@44545
   460
              gfx.setColor(color)
wenzelm@44545
   461
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@44545
   462
            }
wenzelm@44545
   463
wenzelm@49357
   464
            // highlight range -- potentially from other snapshot
wenzelm@46205
   465
            for {
wenzelm@49410
   466
              info <- highlight_area.info
wenzelm@46205
   467
              Text.Info(range, color) <- info.try_restrict(line_range)
wenzelm@49409
   468
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@46205
   469
            } {
wenzelm@46205
   470
              gfx.setColor(color)
wenzelm@46205
   471
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@43435
   472
            }
wenzelm@48921
   473
wenzelm@48921
   474
            // hyperlink range -- potentially from other snapshot
wenzelm@48921
   475
            for {
wenzelm@49410
   476
              info <- hyperlink_area.info
wenzelm@48921
   477
              Text.Info(range, _) <- info.try_restrict(line_range)
wenzelm@49409
   478
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@48921
   479
            } {
wenzelm@49356
   480
              gfx.setColor(rendering.hyperlink_color)
wenzelm@48921
   481
              gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
wenzelm@48921
   482
            }
wenzelm@55688
   483
wenzelm@55688
   484
            // completion range
wenzelm@55747
   485
            if (!hyperlink_area.is_active && caret_visible) {
wenzelm@55747
   486
              for {
wenzelm@55747
   487
                completion <- Completion_Popup.Text_Area(text_area)
wenzelm@55747
   488
                Text.Info(range, color) <- completion.rendering(rendering, line_range)
wenzelm@55747
   489
                r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@55747
   490
              } {
wenzelm@55747
   491
                gfx.setColor(color)
wenzelm@55747
   492
                gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
wenzelm@55711
   493
              }
wenzelm@55688
   494
            }
wenzelm@43435
   495
          }
wenzelm@43435
   496
        }
wenzelm@43435
   497
      }
wenzelm@43435
   498
    }
wenzelm@43435
   499
  }
wenzelm@43435
   500
wenzelm@43435
   501
wenzelm@43393
   502
  /* caret -- outside of text range */
wenzelm@43393
   503
wenzelm@43393
   504
  private class Caret_Painter(before: Boolean) extends TextAreaExtension
wenzelm@43393
   505
  {
wenzelm@43393
   506
    override def paintValidLine(gfx: Graphics2D,
wenzelm@43393
   507
      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
wenzelm@43393
   508
    {
wenzelm@49356
   509
      robust_rendering { _ =>
wenzelm@43404
   510
        if (before) gfx.clipRect(0, 0, 0, 0)
wenzelm@43404
   511
        else gfx.setClip(painter_clip)
wenzelm@43404
   512
      }
wenzelm@43393
   513
    }
wenzelm@43393
   514
  }
wenzelm@43393
   515
wenzelm@43393
   516
  private val before_caret_painter1 = new Caret_Painter(true)
wenzelm@43393
   517
  private val after_caret_painter1 = new Caret_Painter(false)
wenzelm@43393
   518
  private val before_caret_painter2 = new Caret_Painter(true)
wenzelm@43393
   519
  private val after_caret_painter2 = new Caret_Painter(false)
wenzelm@43393
   520
wenzelm@43393
   521
  private val caret_painter = new TextAreaExtension
wenzelm@43393
   522
  {
wenzelm@43393
   523
    override def paintValidLine(gfx: Graphics2D,
wenzelm@43393
   524
      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
wenzelm@43393
   525
    {
wenzelm@55713
   526
      robust_rendering { rendering =>
wenzelm@55713
   527
        if (caret_visible) {
wenzelm@43398
   528
          val caret = text_area.getCaretPosition
wenzelm@43398
   529
          if (start <= caret && caret == end - 1) {
wenzelm@43398
   530
            val painter = text_area.getPainter
wenzelm@43398
   531
            val fm = painter.getFontMetrics
wenzelm@51492
   532
            val metric = JEdit_Lib.pretty_metric(painter)
wenzelm@43393
   533
wenzelm@43398
   534
            val offset = caret - text_area.getLineStartOffset(physical_line)
wenzelm@43398
   535
            val x = text_area.offsetToXY(physical_line, offset).x
wenzelm@55747
   536
            gfx.setColor(caret_color(rendering))
wenzelm@51492
   537
            gfx.drawRect(x, y, (metric.unit * metric.average).round.toInt - 1, fm.getHeight - 1)
wenzelm@43398
   538
          }
wenzelm@43393
   539
        }
wenzelm@43393
   540
      }
wenzelm@43393
   541
    }
wenzelm@43393
   542
  }
wenzelm@43393
   543
wenzelm@43393
   544
wenzelm@43369
   545
  /* activation */
wenzelm@43369
   546
wenzelm@43369
   547
  def activate()
wenzelm@43369
   548
  {
wenzelm@43369
   549
    val painter = text_area.getPainter
wenzelm@43393
   550
    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
wenzelm@43381
   551
    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
wenzelm@43381
   552
    painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
wenzelm@43393
   553
    painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
wenzelm@43393
   554
    painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
wenzelm@43393
   555
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
wenzelm@43393
   556
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
wenzelm@43393
   557
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
wenzelm@43435
   558
    painter.addExtension(500, foreground_painter)
wenzelm@43393
   559
    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
wenzelm@43369
   560
    painter.removeExtension(orig_text_painter)
wenzelm@49410
   561
    painter.addMouseListener(mouse_listener)
wenzelm@49410
   562
    painter.addMouseMotionListener(mouse_motion_listener)
wenzelm@49410
   563
    text_area.addFocusListener(focus_listener)
wenzelm@49410
   564
    view.addWindowListener(window_listener)
wenzelm@43369
   565
  }
wenzelm@43369
   566
wenzelm@43369
   567
  def deactivate()
wenzelm@43369
   568
  {
wenzelm@43369
   569
    val painter = text_area.getPainter
wenzelm@49410
   570
    view.removeWindowListener(window_listener)
wenzelm@49410
   571
    text_area.removeFocusListener(focus_listener)
wenzelm@49410
   572
    painter.removeMouseMotionListener(mouse_motion_listener)
wenzelm@49410
   573
    painter.removeMouseListener(mouse_listener)
wenzelm@43396
   574
    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
wenzelm@43393
   575
    painter.removeExtension(reset_state)
wenzelm@43435
   576
    painter.removeExtension(foreground_painter)
wenzelm@43393
   577
    painter.removeExtension(caret_painter)
wenzelm@43393
   578
    painter.removeExtension(after_caret_painter2)
wenzelm@43393
   579
    painter.removeExtension(before_caret_painter2)
wenzelm@43393
   580
    painter.removeExtension(after_caret_painter1)
wenzelm@43393
   581
    painter.removeExtension(before_caret_painter1)
wenzelm@43381
   582
    painter.removeExtension(text_painter)
wenzelm@43381
   583
    painter.removeExtension(background_painter)
wenzelm@43393
   584
    painter.removeExtension(set_state)
wenzelm@43369
   585
  }
wenzelm@43369
   586
}
wenzelm@43369
   587