src/Tools/jEdit/src/rich_text_area.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64621 7116f2634e32
child 64884 b2e78c0ce537
permissions -rw-r--r--
tuned signature;
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@56322
    13
import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo}
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@56322
    17
import javax.swing.SwingUtilities
wenzelm@43392
    18
import java.text.AttributedString
wenzelm@43369
    19
import java.util.ArrayList
wenzelm@43369
    20
wenzelm@56883
    21
import scala.util.matching.Regex
wenzelm@56883
    22
wenzelm@49410
    23
import org.gjt.sp.util.Log
wenzelm@49410
    24
import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
wenzelm@43369
    25
import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
wenzelm@49410
    26
import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
wenzelm@49410
    27
wenzelm@49410
    28
wenzelm@49492
    29
class Rich_Text_Area(
wenzelm@49492
    30
  view: View,
wenzelm@49492
    31
  text_area: TextArea,
wenzelm@64621
    32
  get_rendering: () => JEdit_Rendering,
wenzelm@50915
    33
  close_action: () => Unit,
wenzelm@56883
    34
  get_search_pattern: () => Option[Regex],
wenzelm@63028
    35
  caret_update: () => Unit,
wenzelm@50306
    36
  caret_visible: Boolean,
wenzelm@53179
    37
  enable_hovering: Boolean)
wenzelm@49410
    38
{
wenzelm@49410
    39
  private val buffer = text_area.getBuffer
wenzelm@43369
    40
wenzelm@43369
    41
wenzelm@49410
    42
  /* robust extension body */
wenzelm@49410
    43
wenzelm@49410
    44
  def robust_body[A](default: A)(body: => A): A =
wenzelm@49410
    45
  {
wenzelm@49410
    46
    try {
wenzelm@57612
    47
      GUI_Thread.require {}
wenzelm@49410
    48
      if (buffer == text_area.getBuffer) body
wenzelm@49410
    49
      else {
wenzelm@49410
    50
        Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
wenzelm@49410
    51
        default
wenzelm@49410
    52
      }
wenzelm@49410
    53
    }
wenzelm@50641
    54
    catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default }
wenzelm@49410
    55
  }
wenzelm@43376
    56
wenzelm@43392
    57
wenzelm@43392
    58
  /* original painters */
wenzelm@43392
    59
wenzelm@43392
    60
  private def pick_extension(name: String): TextAreaExtension =
wenzelm@43369
    61
  {
wenzelm@43369
    62
    text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
wenzelm@43369
    63
    match {
wenzelm@43369
    64
      case List(x) => x
wenzelm@43369
    65
      case _ => error("Expected exactly one " + name)
wenzelm@43369
    66
    }
wenzelm@43369
    67
  }
wenzelm@43369
    68
wenzelm@43392
    69
  private val orig_text_painter =
wenzelm@43392
    70
    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
wenzelm@43392
    71
wenzelm@43392
    72
wenzelm@43393
    73
  /* common painter state */
wenzelm@43381
    74
wenzelm@64621
    75
  @volatile private var painter_rendering: JEdit_Rendering = null
wenzelm@43393
    76
  @volatile private var painter_clip: Shape = null
wenzelm@62988
    77
  @volatile private var caret_focus: Set[Long] = Set.empty
wenzelm@43381
    78
wenzelm@43393
    79
  private val set_state = new TextAreaExtension
wenzelm@43381
    80
  {
wenzelm@43381
    81
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
    82
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
    83
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
    84
    {
wenzelm@49410
    85
      painter_rendering = get_rendering()
wenzelm@46220
    86
      painter_clip = gfx.getClip
wenzelm@62988
    87
      caret_focus =
wenzelm@62988
    88
        JEdit_Lib.visible_range(text_area) match {
wenzelm@63044
    89
          case Some(visible_range) if caret_enabled && !painter_rendering.snapshot.is_outdated =>
wenzelm@62988
    90
            painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range)
wenzelm@62988
    91
          case _ => Set.empty[Long]
wenzelm@62988
    92
        }
wenzelm@43381
    93
    }
wenzelm@43381
    94
  }
wenzelm@43381
    95
wenzelm@43393
    96
  private val reset_state = new TextAreaExtension
wenzelm@43369
    97
  {
wenzelm@43381
    98
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
    99
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
   100
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
   101
    {
wenzelm@49356
   102
      painter_rendering = null
wenzelm@46220
   103
      painter_clip = null
wenzelm@62988
   104
      caret_focus = Set.empty
wenzelm@43381
   105
    }
wenzelm@43381
   106
  }
wenzelm@43381
   107
wenzelm@64621
   108
  def robust_rendering(body: JEdit_Rendering => Unit)
wenzelm@46220
   109
  {
wenzelm@49410
   110
    robust_body(()) { body(painter_rendering) }
wenzelm@49410
   111
  }
wenzelm@49410
   112
wenzelm@49410
   113
wenzelm@49410
   114
  /* active areas within the text */
wenzelm@49410
   115
wenzelm@56317
   116
  private class Active_Area[A](
wenzelm@64621
   117
    rendering: JEdit_Rendering => Text.Range => Option[Text.Info[A]],
wenzelm@56317
   118
    cursor: Option[Int])
wenzelm@49410
   119
  {
wenzelm@49493
   120
    private var the_text_info: Option[(String, Text.Info[A])] = None
wenzelm@49410
   121
wenzelm@55688
   122
    def is_active: Boolean = the_text_info.isDefined
wenzelm@49493
   123
    def text_info: Option[(String, Text.Info[A])] = the_text_info
wenzelm@49493
   124
    def info: Option[Text.Info[A]] = the_text_info.map(_._2)
wenzelm@49410
   125
wenzelm@49410
   126
    def update(new_info: Option[Text.Info[A]])
wenzelm@49410
   127
    {
wenzelm@49493
   128
      val old_text_info = the_text_info
wenzelm@49493
   129
      val new_text_info =
wenzelm@49493
   130
        new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
wenzelm@49493
   131
wenzelm@49493
   132
      if (new_text_info != old_text_info) {
wenzelm@63028
   133
        caret_update()
wenzelm@56317
   134
        if (cursor.isDefined) {
wenzelm@56317
   135
          if (new_text_info.isDefined)
wenzelm@56317
   136
            text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get))
wenzelm@56317
   137
          else
wenzelm@56406
   138
            text_area.getPainter.resetCursor()
wenzelm@56317
   139
        }
wenzelm@49493
   140
        for {
wenzelm@49493
   141
          r0 <- JEdit_Lib.visible_range(text_area)
wenzelm@49493
   142
          opt <- List(old_text_info, new_text_info)
wenzelm@49493
   143
          (_, Text.Info(r1, _)) <- opt
wenzelm@49493
   144
          r2 <- r1.try_restrict(r0)  // FIXME more precise?!
wenzelm@49493
   145
        } JEdit_Lib.invalidate_range(text_area, r2)
wenzelm@49493
   146
        the_text_info = new_text_info
wenzelm@49410
   147
      }
wenzelm@49410
   148
    }
wenzelm@49410
   149
wenzelm@64621
   150
    def update_rendering(r: JEdit_Rendering, range: Text.Range)
wenzelm@49410
   151
    { update(rendering(r)(range)) }
wenzelm@49410
   152
wenzelm@49410
   153
    def reset { update(None) }
wenzelm@49410
   154
  }
wenzelm@49410
   155
wenzelm@57612
   156
  // owned by GUI thread
wenzelm@49410
   157
wenzelm@56317
   158
  private val highlight_area =
wenzelm@60892
   159
    new Active_Area[Color](
wenzelm@64621
   160
      (rendering: JEdit_Rendering) => rendering.highlight _, None)
wenzelm@60892
   161
wenzelm@52980
   162
  private val hyperlink_area =
wenzelm@56317
   163
    new Active_Area[PIDE.editor.Hyperlink](
wenzelm@64621
   164
      (rendering: JEdit_Rendering) => rendering.hyperlink _, Some(Cursor.HAND_CURSOR))
wenzelm@60892
   165
wenzelm@56317
   166
  private val active_area =
wenzelm@60892
   167
    new Active_Area[XML.Elem](
wenzelm@64621
   168
      (rendering: JEdit_Rendering) => rendering.active _, Some(Cursor.DEFAULT_CURSOR))
wenzelm@49492
   169
wenzelm@49492
   170
  private val active_areas =
wenzelm@50450
   171
    List((highlight_area, true), (hyperlink_area, true), (active_area, false))
wenzelm@50216
   172
  def active_reset(): Unit = active_areas.foreach(_._1.reset)
wenzelm@49410
   173
wenzelm@62988
   174
  private def area_active(): Boolean =
wenzelm@62988
   175
    active_areas.exists({ case (area, _) => area.is_active })
wenzelm@62988
   176
wenzelm@49410
   177
  private val focus_listener = new FocusAdapter {
wenzelm@49424
   178
    override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
wenzelm@49410
   179
  }
wenzelm@49410
   180
wenzelm@49410
   181
  private val window_listener = new WindowAdapter {
wenzelm@49424
   182
    override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } }
wenzelm@49424
   183
    override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } }
wenzelm@49410
   184
  }
wenzelm@49410
   185
wenzelm@49410
   186
  private val mouse_listener = new MouseAdapter {
wenzelm@49410
   187
    override def mouseClicked(e: MouseEvent) {
wenzelm@49424
   188
      robust_body(()) {
wenzelm@49424
   189
        hyperlink_area.info match {
wenzelm@56433
   190
          case Some(Text.Info(range, link)) =>
wenzelm@56494
   191
            if (!link.external) {
wenzelm@56494
   192
              try { text_area.moveCaretPosition(range.start) }
wenzelm@56494
   193
              catch {
wenzelm@56494
   194
                case _: ArrayIndexOutOfBoundsException =>
wenzelm@56494
   195
                case _: IllegalArgumentException =>
wenzelm@56494
   196
              }
wenzelm@56494
   197
              text_area.requestFocus
wenzelm@56433
   198
            }
wenzelm@52482
   199
            link.follow(view)
wenzelm@49492
   200
          case None =>
wenzelm@49492
   201
        }
wenzelm@50450
   202
        active_area.text_info match {
wenzelm@50915
   203
          case Some((text, Text.Info(_, markup))) =>
wenzelm@50915
   204
            Active.action(view, text, markup)
wenzelm@50915
   205
            close_action()
wenzelm@49424
   206
          case None =>
wenzelm@49424
   207
        }
wenzelm@49410
   208
      }
wenzelm@49410
   209
    }
wenzelm@49410
   210
  }
wenzelm@49410
   211
wenzelm@56322
   212
  private def mouse_inside_painter(): Boolean =
wenzelm@56322
   213
    MouseInfo.getPointerInfo match {
wenzelm@56322
   214
      case null => false
wenzelm@56322
   215
      case info =>
wenzelm@56322
   216
        val point = info.getLocation
wenzelm@56322
   217
        val painter = text_area.getPainter
wenzelm@56322
   218
        SwingUtilities.convertPointFromScreen(point, painter)
wenzelm@56322
   219
        painter.contains(point)
wenzelm@56322
   220
    }
wenzelm@56322
   221
wenzelm@49410
   222
  private val mouse_motion_listener = new MouseMotionAdapter {
wenzelm@56321
   223
    override def mouseDragged(evt: MouseEvent) {
wenzelm@56321
   224
      robust_body(()) {
wenzelm@57857
   225
        active_reset()
wenzelm@56497
   226
        Completion_Popup.Text_Area.dismissed(text_area)
wenzelm@56497
   227
        Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
wenzelm@56321
   228
      }
wenzelm@56321
   229
    }
wenzelm@56321
   230
wenzelm@53182
   231
    override def mouseMoved(evt: MouseEvent) {
wenzelm@49424
   232
      robust_body(()) {
wenzelm@53182
   233
        val x = evt.getX
wenzelm@53182
   234
        val y = evt.getY
wenzelm@53182
   235
        val control = (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
wenzelm@49492
   236
wenzelm@53179
   237
        if ((control || enable_hovering) && !buffer.isLoading) {
wenzelm@49424
   238
          JEdit_Lib.buffer_lock(buffer) {
wenzelm@53182
   239
            JEdit_Lib.pixel_range(text_area, x, y) match {
wenzelm@50211
   240
              case None => active_reset()
wenzelm@49941
   241
              case Some(range) =>
wenzelm@49941
   242
                val rendering = get_rendering()
wenzelm@49941
   243
                for ((area, require_control) <- active_areas)
wenzelm@49941
   244
                {
wenzelm@50165
   245
                  if (control == require_control && !rendering.snapshot.is_outdated)
wenzelm@49941
   246
                    area.update_rendering(rendering, range)
wenzelm@49941
   247
                  else area.reset
wenzelm@49941
   248
                }
wenzelm@49492
   249
            }
wenzelm@49424
   250
          }
wenzelm@49410
   251
        }
wenzelm@49424
   252
        else active_reset()
wenzelm@51441
   253
wenzelm@53182
   254
        if (evt.getSource == text_area.getPainter) {
wenzelm@52494
   255
          Pretty_Tooltip.invoke(() =>
wenzelm@52495
   256
            robust_body(()) {
wenzelm@56322
   257
              if (mouse_inside_painter()) {
wenzelm@56322
   258
                val rendering = get_rendering()
wenzelm@56322
   259
                val snapshot = rendering.snapshot
wenzelm@56322
   260
                if (!snapshot.is_outdated) {
wenzelm@56322
   261
                  JEdit_Lib.pixel_range(text_area, x, y) match {
wenzelm@56322
   262
                    case None =>
wenzelm@56322
   263
                    case Some(range) =>
wenzelm@56322
   264
                      val result =
wenzelm@56322
   265
                        if (control) rendering.tooltip(range)
wenzelm@56322
   266
                        else rendering.tooltip_message(range)
wenzelm@56322
   267
                      result match {
wenzelm@56322
   268
                        case None =>
wenzelm@56322
   269
                        case Some(tip) =>
wenzelm@56322
   270
                          val painter = text_area.getPainter
wenzelm@58767
   271
                          val loc = new Point(x, y + painter.getLineHeight / 2)
wenzelm@56496
   272
                          val results = rendering.command_results(tip.range)
wenzelm@56322
   273
                          Pretty_Tooltip(view, painter, loc, rendering, results, tip)
wenzelm@56322
   274
                      }
wenzelm@56322
   275
                  }
wenzelm@52494
   276
                }
wenzelm@52494
   277
              }
wenzelm@52495
   278
          })
wenzelm@51452
   279
        }
wenzelm@49410
   280
      }
wenzelm@49410
   281
    }
wenzelm@49410
   282
  }
wenzelm@49410
   283
wenzelm@49410
   284
wenzelm@55713
   285
  /* text background */
wenzelm@55713
   286
wenzelm@43381
   287
  private val background_painter = new TextAreaExtension
wenzelm@43381
   288
  {
wenzelm@43381
   289
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
   290
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
   291
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
   292
    {
wenzelm@49356
   293
      robust_rendering { rendering =>
wenzelm@51581
   294
        val fm = text_area.getPainter.getFontMetrics
wenzelm@43376
   295
wenzelm@43381
   296
        for (i <- 0 until physical_lines.length) {
wenzelm@43381
   297
          if (physical_lines(i) != -1) {
wenzelm@56884
   298
            val line_range = Text.Range(start(i), end(i) min buffer.getLength)
wenzelm@43376
   299
wenzelm@49473
   300
            // line background color
wenzelm@49473
   301
            for { (color, separator) <- rendering.line_background(line_range) }
wenzelm@49473
   302
            {
wenzelm@49473
   303
              gfx.setColor(color)
wenzelm@60215
   304
              val sep = if (separator) 2 min (line_height / 2) else 0
wenzelm@49475
   305
              gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
wenzelm@49473
   306
            }
wenzelm@49473
   307
wenzelm@55790
   308
            // background color
wenzelm@43381
   309
            for {
wenzelm@62988
   310
              Text.Info(range, color) <- rendering.background(line_range, caret_focus)
wenzelm@49409
   311
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@43381
   312
            } {
wenzelm@43381
   313
              gfx.setColor(color)
wenzelm@43381
   314
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@43381
   315
            }
wenzelm@43376
   316
wenzelm@50450
   317
            // active area -- potentially from other snapshot
wenzelm@49492
   318
            for {
wenzelm@50450
   319
              info <- active_area.info
wenzelm@49492
   320
              Text.Info(range, _) <- info.try_restrict(line_range)
wenzelm@49492
   321
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@49492
   322
            } {
wenzelm@50450
   323
              gfx.setColor(rendering.active_hover_color)
wenzelm@49492
   324
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@49492
   325
            }
wenzelm@49492
   326
wenzelm@43381
   327
            // squiggly underline
wenzelm@43381
   328
            for {
wenzelm@49356
   329
              Text.Info(range, color) <- rendering.squiggly_underline(line_range)
wenzelm@49409
   330
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@43381
   331
            } {
wenzelm@43381
   332
              gfx.setColor(color)
wenzelm@43381
   333
              val x0 = (r.x / 2) * 2
wenzelm@51574
   334
              val y0 = r.y + fm.getAscent + 1
wenzelm@43381
   335
              for (x1 <- Range(x0, x0 + r.length, 2)) {
wenzelm@43381
   336
                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
wenzelm@43381
   337
                gfx.drawLine(x1, y1, x1 + 1, y1)
wenzelm@43376
   338
              }
wenzelm@43376
   339
            }
wenzelm@56550
   340
wenzelm@56560
   341
            // spell checker
wenzelm@56550
   342
            for {
wenzelm@56558
   343
              spell_checker <- PIDE.spell_checker.get
wenzelm@56565
   344
              spell_range <- rendering.spell_checker_ranges(line_range)
wenzelm@56565
   345
              text <- JEdit_Lib.try_get_text(buffer, spell_range)
wenzelm@56565
   346
              info <- spell_checker.marked_words(spell_range.start, text)
wenzelm@56565
   347
              r <- JEdit_Lib.gfx_range(text_area, info.range)
wenzelm@56550
   348
            } {
wenzelm@56550
   349
              gfx.setColor(rendering.spell_checker_color)
wenzelm@56560
   350
              val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2))
wenzelm@56550
   351
              gfx.drawLine(r.x, y0, r.x + r.length, y0)
wenzelm@56550
   352
            }
wenzelm@43376
   353
          }
wenzelm@43376
   354
        }
wenzelm@43376
   355
      }
wenzelm@43381
   356
    }
wenzelm@43381
   357
  }
wenzelm@43381
   358
wenzelm@43381
   359
wenzelm@43381
   360
  /* text */
wenzelm@43369
   361
wenzelm@55766
   362
  private def caret_enabled: Boolean =
wenzelm@55766
   363
    caret_visible && (!text_area.hasFocus || text_area.isCaretVisible)
wenzelm@55766
   364
wenzelm@64621
   365
  private def caret_color(rendering: JEdit_Rendering, offset: Text.Offset): Color =
wenzelm@55747
   366
  {
wenzelm@61011
   367
    if (text_area.isCaretVisible) text_area.getPainter.getCaretColor
wenzelm@61014
   368
    else {
wenzelm@61014
   369
      val debug_positions =
wenzelm@61017
   370
        (for {
wenzelm@61017
   371
          c <- Debugger.focus().iterator
wenzelm@61017
   372
          pos <- c.debug_position.iterator
wenzelm@61017
   373
        } yield pos).toList
wenzelm@61014
   374
      if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))
wenzelm@61011
   375
        rendering.caret_debugger_color
wenzelm@61011
   376
      else rendering.caret_invisible_color
wenzelm@61014
   377
    }
wenzelm@55747
   378
  }
wenzelm@55747
   379
wenzelm@64621
   380
  private def paint_chunk_list(rendering: JEdit_Rendering,
wenzelm@43505
   381
    gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
wenzelm@43382
   382
  {
wenzelm@43382
   383
    val clip_rect = gfx.getClipBounds
wenzelm@43392
   384
    val painter = text_area.getPainter
wenzelm@43392
   385
    val font_context = painter.getFontRenderContext
wenzelm@55747
   386
wenzelm@55747
   387
    val caret_range =
wenzelm@56592
   388
      if (caret_enabled) JEdit_Lib.caret_range(text_area)
wenzelm@56172
   389
      else Text.Range.offside
wenzelm@43382
   390
wenzelm@43382
   391
    var w = 0.0f
wenzelm@43382
   392
    var chunk = head
wenzelm@43382
   393
    while (chunk != null) {
wenzelm@43505
   394
      val chunk_offset = line_start + chunk.offset
wenzelm@43382
   395
      if (x + w + chunk.width > clip_rect.x &&
wenzelm@50306
   396
          x + w < clip_rect.x + clip_rect.width && chunk.length > 0)
wenzelm@43382
   397
      {
wenzelm@43505
   398
        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
wenzelm@44662
   399
        val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
wenzelm@43382
   400
        val chunk_font = chunk.style.getFont
wenzelm@43382
   401
        val chunk_color = chunk.style.getForegroundColor
wenzelm@43382
   402
wenzelm@44056
   403
        def string_width(s: String): Float =
wenzelm@44056
   404
          if (s.isEmpty) 0.0f
wenzelm@44056
   405
          else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
wenzelm@44056
   406
wenzelm@43426
   407
        val markup =
wenzelm@43428
   408
          for {
wenzelm@49356
   409
            r1 <- rendering.text_color(chunk_range, chunk_color)
wenzelm@43450
   410
            r2 <- r1.try_restrict(chunk_range)
wenzelm@43450
   411
          } yield r2
wenzelm@43382
   412
wenzelm@56373
   413
        val padded_markup_iterator =
wenzelm@43759
   414
          if (markup.isEmpty)
wenzelm@46197
   415
            Iterator(Text.Info(chunk_range, chunk_color))
wenzelm@43759
   416
          else
wenzelm@46197
   417
            Iterator(
wenzelm@46197
   418
              Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
wenzelm@43759
   419
            markup.iterator ++
wenzelm@46197
   420
            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
wenzelm@43759
   421
wenzelm@43450
   422
        var x1 = x + w
wenzelm@43382
   423
        gfx.setFont(chunk_font)
wenzelm@56373
   424
        for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) {
wenzelm@44662
   425
          val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
wenzelm@46197
   426
          gfx.setColor(color)
wenzelm@43448
   427
wenzelm@43759
   428
          range.try_restrict(caret_range) match {
wenzelm@43759
   429
            case Some(r) if !r.is_singularity =>
wenzelm@43759
   430
              val i = r.start - range.start
wenzelm@43759
   431
              val j = r.stop - range.start
wenzelm@44056
   432
              val s1 = str.substring(0, i)
wenzelm@44056
   433
              val s2 = str.substring(i, j)
wenzelm@44056
   434
              val s3 = str.substring(j)
wenzelm@44056
   435
wenzelm@62812
   436
              if (s1.nonEmpty) gfx.drawString(Word.bidi_override(s1), x1, y)
wenzelm@44056
   437
wenzelm@62812
   438
              val astr = new AttributedString(Word.bidi_override(s2))
wenzelm@43759
   439
              astr.addAttribute(TextAttribute.FONT, chunk_font)
wenzelm@61011
   440
              astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, r.start))
wenzelm@44056
   441
              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
wenzelm@44056
   442
              gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
wenzelm@44056
   443
wenzelm@59319
   444
              if (s3.nonEmpty)
wenzelm@62812
   445
                gfx.drawString(Word.bidi_override(s3), x1 + string_width(str.substring(0, j)), y)
wenzelm@44056
   446
wenzelm@43759
   447
            case _ =>
wenzelm@62812
   448
              gfx.drawString(Word.bidi_override(str), x1, y)
wenzelm@43382
   449
          }
wenzelm@44056
   450
          x1 += string_width(str)
wenzelm@43382
   451
        }
wenzelm@43382
   452
      }
wenzelm@43382
   453
      w += chunk.width
wenzelm@43382
   454
      chunk = chunk.next.asInstanceOf[Chunk]
wenzelm@43382
   455
    }
wenzelm@43382
   456
    w
wenzelm@43382
   457
  }
wenzelm@43382
   458
wenzelm@43381
   459
  private val text_painter = new TextAreaExtension
wenzelm@43381
   460
  {
wenzelm@43381
   461
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
   462
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43382
   463
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
   464
    {
wenzelm@49356
   465
      robust_rendering { rendering =>
wenzelm@51581
   466
        val painter = text_area.getPainter
wenzelm@51581
   467
        val fm = painter.getFontMetrics
wenzelm@51581
   468
        val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext)
wenzelm@51581
   469
wenzelm@43381
   470
        val clip = gfx.getClip
wenzelm@43381
   471
        val x0 = text_area.getHorizontalOffset
wenzelm@58767
   472
        var y0 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent
wenzelm@43372
   473
wenzelm@51581
   474
        val (bullet_x, bullet_y, bullet_w, bullet_h) =
wenzelm@51581
   475
        {
wenzelm@51581
   476
          val w = fm.charWidth(' ')
wenzelm@51581
   477
          val b = (w / 2) max 1
wenzelm@51581
   478
          val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt
wenzelm@51581
   479
          ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
wenzelm@51581
   480
        }
wenzelm@51581
   481
wenzelm@43381
   482
        for (i <- 0 until physical_lines.length) {
wenzelm@49097
   483
          val line = physical_lines(i)
wenzelm@49097
   484
          if (line != -1) {
wenzelm@56884
   485
            val line_range = Text.Range(start(i), end(i) min buffer.getLength)
wenzelm@51581
   486
wenzelm@51581
   487
            // text chunks
wenzelm@49097
   488
            val screen_line = first_line + i
wenzelm@49097
   489
            val chunks = text_area.getChunksOfScreenLine(screen_line)
wenzelm@49097
   490
            if (chunks != null) {
wenzelm@56358
   491
              try {
wenzelm@56358
   492
                val line_start = buffer.getLineStartOffset(line)
wenzelm@56358
   493
                gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
wenzelm@56358
   494
                val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
wenzelm@56358
   495
                gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
wenzelm@56358
   496
                orig_text_painter.paintValidLine(gfx,
wenzelm@56358
   497
                  screen_line, line, start(i), end(i), y + line_height * i)
wenzelm@56358
   498
              } finally { gfx.setClip(clip) }
wenzelm@49097
   499
            }
wenzelm@60913
   500
wenzelm@60913
   501
            // bullet bar
wenzelm@60913
   502
            for {
wenzelm@60913
   503
              Text.Info(range, color) <- rendering.bullet(line_range)
wenzelm@60913
   504
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@60913
   505
            } {
wenzelm@60913
   506
              gfx.setColor(color)
wenzelm@60913
   507
              gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
wenzelm@60913
   508
                r.length - bullet_w, line_height - bullet_h)
wenzelm@60913
   509
            }
wenzelm@43369
   510
          }
wenzelm@43381
   511
          y0 += line_height
wenzelm@43369
   512
        }
wenzelm@43369
   513
      }
wenzelm@43369
   514
    }
wenzelm@43369
   515
  }
wenzelm@43369
   516
wenzelm@43369
   517
wenzelm@43435
   518
  /* foreground */
wenzelm@43435
   519
wenzelm@43435
   520
  private val foreground_painter = new TextAreaExtension
wenzelm@43435
   521
  {
wenzelm@43435
   522
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43435
   523
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43435
   524
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43435
   525
    {
wenzelm@49356
   526
      robust_rendering { rendering =>
wenzelm@56883
   527
        val search_pattern = get_search_pattern()
wenzelm@43435
   528
        for (i <- 0 until physical_lines.length) {
wenzelm@43435
   529
          if (physical_lines(i) != -1) {
wenzelm@56884
   530
            val line_range = Text.Range(start(i), end(i) min buffer.getLength)
wenzelm@43435
   531
wenzelm@44545
   532
            // foreground color
wenzelm@44545
   533
            for {
wenzelm@49356
   534
              Text.Info(range, color) <- rendering.foreground(line_range)
wenzelm@49409
   535
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@44545
   536
            } {
wenzelm@44545
   537
              gfx.setColor(color)
wenzelm@44545
   538
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@44545
   539
            }
wenzelm@44545
   540
wenzelm@56883
   541
            // search pattern
wenzelm@56883
   542
            for {
wenzelm@56883
   543
              regex <- search_pattern
wenzelm@56883
   544
              text <- JEdit_Lib.try_get_text(buffer, line_range)
wenzelm@56883
   545
              m <- regex.findAllMatchIn(text)
wenzelm@56883
   546
              range = Text.Range(m.start, m.end) + line_range.start
wenzelm@56883
   547
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@56883
   548
            } {
wenzelm@56883
   549
              gfx.setColor(rendering.search_color)
wenzelm@56883
   550
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@56883
   551
            }
wenzelm@56883
   552
wenzelm@49357
   553
            // highlight range -- potentially from other snapshot
wenzelm@46205
   554
            for {
wenzelm@49410
   555
              info <- highlight_area.info
wenzelm@46205
   556
              Text.Info(range, color) <- info.try_restrict(line_range)
wenzelm@49409
   557
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@46205
   558
            } {
wenzelm@46205
   559
              gfx.setColor(color)
wenzelm@46205
   560
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@43435
   561
            }
wenzelm@48921
   562
wenzelm@48921
   563
            // hyperlink range -- potentially from other snapshot
wenzelm@48921
   564
            for {
wenzelm@49410
   565
              info <- hyperlink_area.info
wenzelm@48921
   566
              Text.Info(range, _) <- info.try_restrict(line_range)
wenzelm@49409
   567
              r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@48921
   568
            } {
wenzelm@49356
   569
              gfx.setColor(rendering.hyperlink_color)
wenzelm@48921
   570
              gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
wenzelm@48921
   571
            }
wenzelm@55688
   572
wenzelm@62988
   573
            // entity def range
wenzelm@62988
   574
            if (!area_active() && caret_visible) {
wenzelm@62988
   575
              for {
wenzelm@62991
   576
                Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus)
wenzelm@62988
   577
                r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@62988
   578
              } {
wenzelm@62988
   579
                gfx.setColor(color)
wenzelm@62988
   580
                gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
wenzelm@62988
   581
              }
wenzelm@62988
   582
            }
wenzelm@62988
   583
wenzelm@55688
   584
            // completion range
wenzelm@62988
   585
            if (!area_active() && caret_visible) {
wenzelm@55747
   586
              for {
wenzelm@55747
   587
                completion <- Completion_Popup.Text_Area(text_area)
wenzelm@55747
   588
                Text.Info(range, color) <- completion.rendering(rendering, line_range)
wenzelm@55747
   589
                r <- JEdit_Lib.gfx_range(text_area, range)
wenzelm@55747
   590
              } {
wenzelm@55747
   591
                gfx.setColor(color)
wenzelm@55747
   592
                gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
wenzelm@55711
   593
              }
wenzelm@55688
   594
            }
wenzelm@43435
   595
          }
wenzelm@43435
   596
        }
wenzelm@43435
   597
      }
wenzelm@43435
   598
    }
wenzelm@43435
   599
  }
wenzelm@43435
   600
wenzelm@43435
   601
wenzelm@43393
   602
  /* caret -- outside of text range */
wenzelm@43393
   603
wenzelm@43393
   604
  private class Caret_Painter(before: Boolean) extends TextAreaExtension
wenzelm@43393
   605
  {
wenzelm@43393
   606
    override def paintValidLine(gfx: Graphics2D,
wenzelm@43393
   607
      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
wenzelm@43393
   608
    {
wenzelm@49356
   609
      robust_rendering { _ =>
wenzelm@43404
   610
        if (before) gfx.clipRect(0, 0, 0, 0)
wenzelm@43404
   611
        else gfx.setClip(painter_clip)
wenzelm@43404
   612
      }
wenzelm@43393
   613
    }
wenzelm@43393
   614
  }
wenzelm@43393
   615
wenzelm@43393
   616
  private val before_caret_painter1 = new Caret_Painter(true)
wenzelm@43393
   617
  private val after_caret_painter1 = new Caret_Painter(false)
wenzelm@43393
   618
  private val before_caret_painter2 = new Caret_Painter(true)
wenzelm@43393
   619
  private val after_caret_painter2 = new Caret_Painter(false)
wenzelm@43393
   620
wenzelm@43393
   621
  private val caret_painter = new TextAreaExtension
wenzelm@43393
   622
  {
wenzelm@43393
   623
    override def paintValidLine(gfx: Graphics2D,
wenzelm@43393
   624
      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
wenzelm@43393
   625
    {
wenzelm@55713
   626
      robust_rendering { rendering =>
wenzelm@55713
   627
        if (caret_visible) {
wenzelm@43398
   628
          val caret = text_area.getCaretPosition
wenzelm@55766
   629
          if (caret_enabled && start <= caret && caret == end - 1) {
wenzelm@43398
   630
            val painter = text_area.getPainter
wenzelm@43398
   631
            val fm = painter.getFontMetrics
wenzelm@43393
   632
wenzelm@43398
   633
            val offset = caret - text_area.getLineStartOffset(physical_line)
wenzelm@43398
   634
            val x = text_area.offsetToXY(physical_line, offset).x
wenzelm@58767
   635
            val y1 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent
wenzelm@56358
   636
wenzelm@56358
   637
            val astr = new AttributedString(" ")
wenzelm@56358
   638
            astr.addAttribute(TextAttribute.FONT, painter.getFont)
wenzelm@61011
   639
            astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, caret))
wenzelm@56358
   640
            astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
wenzelm@56358
   641
wenzelm@56358
   642
            val clip = gfx.getClip
wenzelm@56358
   643
            try {
wenzelm@56358
   644
              gfx.clipRect(x, y, Integer.MAX_VALUE, painter.getLineHeight)
wenzelm@56358
   645
              gfx.drawString(astr.getIterator, x, y1)
wenzelm@56358
   646
            }
wenzelm@56358
   647
            finally { gfx.setClip(clip) }
wenzelm@43398
   648
          }
wenzelm@43393
   649
        }
wenzelm@43393
   650
      }
wenzelm@43393
   651
    }
wenzelm@43393
   652
  }
wenzelm@43393
   653
wenzelm@43393
   654
wenzelm@43369
   655
  /* activation */
wenzelm@43369
   656
wenzelm@43369
   657
  def activate()
wenzelm@43369
   658
  {
wenzelm@43369
   659
    val painter = text_area.getPainter
wenzelm@43393
   660
    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
wenzelm@43381
   661
    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
wenzelm@43381
   662
    painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
wenzelm@43393
   663
    painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
wenzelm@43393
   664
    painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
wenzelm@43393
   665
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
wenzelm@43393
   666
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
wenzelm@43393
   667
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
wenzelm@43435
   668
    painter.addExtension(500, foreground_painter)
wenzelm@43393
   669
    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
wenzelm@43369
   670
    painter.removeExtension(orig_text_painter)
wenzelm@49410
   671
    painter.addMouseListener(mouse_listener)
wenzelm@49410
   672
    painter.addMouseMotionListener(mouse_motion_listener)
wenzelm@49410
   673
    text_area.addFocusListener(focus_listener)
wenzelm@49410
   674
    view.addWindowListener(window_listener)
wenzelm@43369
   675
  }
wenzelm@43369
   676
wenzelm@43369
   677
  def deactivate()
wenzelm@43369
   678
  {
wenzelm@56340
   679
    active_reset()
wenzelm@43369
   680
    val painter = text_area.getPainter
wenzelm@49410
   681
    view.removeWindowListener(window_listener)
wenzelm@49410
   682
    text_area.removeFocusListener(focus_listener)
wenzelm@49410
   683
    painter.removeMouseMotionListener(mouse_motion_listener)
wenzelm@49410
   684
    painter.removeMouseListener(mouse_listener)
wenzelm@43396
   685
    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
wenzelm@43393
   686
    painter.removeExtension(reset_state)
wenzelm@43435
   687
    painter.removeExtension(foreground_painter)
wenzelm@43393
   688
    painter.removeExtension(caret_painter)
wenzelm@43393
   689
    painter.removeExtension(after_caret_painter2)
wenzelm@43393
   690
    painter.removeExtension(before_caret_painter2)
wenzelm@43393
   691
    painter.removeExtension(after_caret_painter1)
wenzelm@43393
   692
    painter.removeExtension(before_caret_painter1)
wenzelm@43381
   693
    painter.removeExtension(text_painter)
wenzelm@43381
   694
    painter.removeExtension(background_painter)
wenzelm@43393
   695
    painter.removeExtension(set_state)
wenzelm@43369
   696
  }
wenzelm@43369
   697
}