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