src/Tools/jEdit/src/jedit/document_view.scala
author wenzelm
Tue Sep 07 17:34:28 2010 +0200 (2010-09-07)
changeset 39174 b95cf3892483
parent 39171 525a13b9ac74
child 39175 a08d68e993ea
permissions -rw-r--r--
Document_View: some markup for main inner syntax categories;
wenzelm@36760
     1
/*  Title:      Tools/jEdit/src/jedit/document_view.scala
wenzelm@36760
     2
    Author:     Fabian Immler, TU Munich
wenzelm@36760
     3
    Author:     Makarius
wenzelm@36760
     4
wenzelm@36760
     5
Document view connected to jEdit text area.
wenzelm@36760
     6
*/
wenzelm@34408
     7
immler@34403
     8
package isabelle.jedit
immler@34403
     9
wenzelm@34760
    10
wenzelm@36015
    11
import isabelle._
wenzelm@36015
    12
wenzelm@34784
    13
import scala.actors.Actor._
wenzelm@34784
    14
wenzelm@39131
    15
import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
wenzelm@34784
    16
import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
wenzelm@34734
    17
import javax.swing.{JPanel, ToolTipManager}
wenzelm@34784
    18
import javax.swing.event.{CaretListener, CaretEvent}
wenzelm@34734
    19
wenzelm@39131
    20
import org.gjt.sp.jedit.OperatingSystem
wenzelm@34709
    21
import org.gjt.sp.jedit.gui.RolloverButton
wenzelm@34784
    22
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
wenzelm@37241
    23
import org.gjt.sp.jedit.syntax.SyntaxStyle
wenzelm@34784
    24
wenzelm@34784
    25
wenzelm@34784
    26
object Document_View
wenzelm@34784
    27
{
wenzelm@39044
    28
  /* physical rendering */
wenzelm@39044
    29
wenzelm@39169
    30
  val outdated_color = new Color(240, 240, 240)
wenzelm@39169
    31
  val unfinished_color = new Color(255, 228, 225)
wenzelm@39169
    32
wenzelm@39169
    33
  val regular_color = new Color(192, 192, 192)
wenzelm@39169
    34
  val warning_color = new Color(255, 165, 0)
wenzelm@39169
    35
  val error_color = new Color(255, 106, 106)
wenzelm@39171
    36
  val bad_color = new Color(255, 204, 153, 100)
wenzelm@39169
    37
wenzelm@39169
    38
  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@34784
    39
  {
wenzelm@38356
    40
    val state = snapshot.state(command)
wenzelm@39169
    41
    if (snapshot.is_outdated) Some(outdated_color)
wenzelm@37186
    42
    else
wenzelm@38567
    43
      Isar_Document.command_status(state.status) match {
wenzelm@39169
    44
        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
wenzelm@39169
    45
        case Isar_Document.Unprocessed => Some(unfinished_color)
wenzelm@39169
    46
        case _ => None
wenzelm@37186
    47
      }
wenzelm@34784
    48
  }
wenzelm@34784
    49
wenzelm@39169
    50
  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@39169
    51
  {
wenzelm@39169
    52
    val state = snapshot.state(command)
wenzelm@39169
    53
    if (snapshot.is_outdated) None
wenzelm@39169
    54
    else
wenzelm@39169
    55
      Isar_Document.command_status(state.status) match {
wenzelm@39169
    56
        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
wenzelm@39169
    57
        case Isar_Document.Unprocessed => Some(unfinished_color)
wenzelm@39169
    58
        case Isar_Document.Failed => Some(error_color)
wenzelm@39169
    59
        case _ => None
wenzelm@39169
    60
      }
wenzelm@39169
    61
  }
wenzelm@39169
    62
wenzelm@39169
    63
wenzelm@39174
    64
  /* markup selectors */
wenzelm@39174
    65
wenzelm@39174
    66
  private val message_markup: PartialFunction[Text.Info[Any], Color] =
wenzelm@39044
    67
  {
wenzelm@39169
    68
    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
wenzelm@39169
    69
    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
wenzelm@39169
    70
    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
wenzelm@39044
    71
  }
wenzelm@39044
    72
wenzelm@39174
    73
  private val background_markup: PartialFunction[Text.Info[Any], Color] =
wenzelm@39171
    74
  {
wenzelm@39171
    75
    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
wenzelm@39171
    76
  }
wenzelm@39171
    77
wenzelm@39174
    78
  private val box_markup: PartialFunction[Text.Info[Any], Color] =
wenzelm@39168
    79
  {
wenzelm@39169
    80
    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
wenzelm@39168
    81
  }
wenzelm@39168
    82
wenzelm@39174
    83
  private val tooltip_markup: PartialFunction[Text.Info[Any], String] =
wenzelm@39174
    84
  {
wenzelm@39174
    85
    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
wenzelm@39174
    86
      Pretty.string_of(List(Pretty.block(body)), margin = 40)
wenzelm@39174
    87
    case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
wenzelm@39174
    88
    case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
wenzelm@39174
    89
    case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
wenzelm@39174
    90
    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
wenzelm@39174
    91
  }
wenzelm@39174
    92
wenzelm@34784
    93
wenzelm@34784
    94
  /* document view of text area */
wenzelm@34784
    95
wenzelm@34784
    96
  private val key = new Object
wenzelm@34784
    97
wenzelm@34784
    98
  def init(model: Document_Model, text_area: TextArea): Document_View =
wenzelm@34784
    99
  {
wenzelm@38223
   100
    Swing_Thread.require()
wenzelm@34784
   101
    val doc_view = new Document_View(model, text_area)
wenzelm@34784
   102
    text_area.putClientProperty(key, doc_view)
wenzelm@34784
   103
    doc_view.activate()
wenzelm@34784
   104
    doc_view
wenzelm@34784
   105
  }
wenzelm@34784
   106
wenzelm@34788
   107
  def apply(text_area: TextArea): Option[Document_View] =
wenzelm@34784
   108
  {
wenzelm@38223
   109
    Swing_Thread.require()
wenzelm@34784
   110
    text_area.getClientProperty(key) match {
wenzelm@34784
   111
      case doc_view: Document_View => Some(doc_view)
wenzelm@34784
   112
      case _ => None
wenzelm@34784
   113
    }
wenzelm@34784
   114
  }
wenzelm@34784
   115
wenzelm@34784
   116
  def exit(text_area: TextArea)
wenzelm@34784
   117
  {
wenzelm@38223
   118
    Swing_Thread.require()
wenzelm@34788
   119
    apply(text_area) match {
wenzelm@34784
   120
      case None => error("No document view for text area: " + text_area)
wenzelm@34784
   121
      case Some(doc_view) =>
wenzelm@34784
   122
        doc_view.deactivate()
wenzelm@34784
   123
        text_area.putClientProperty(key, null)
wenzelm@34784
   124
    }
wenzelm@34784
   125
  }
wenzelm@34784
   126
}
immler@34403
   127
wenzelm@34733
   128
wenzelm@37129
   129
class Document_View(val model: Document_Model, text_area: TextArea)
immler@34654
   130
{
wenzelm@34784
   131
  private val session = model.session
wenzelm@34784
   132
immler@34403
   133
wenzelm@37241
   134
  /* extended token styles */
wenzelm@37241
   135
wenzelm@37241
   136
  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
wenzelm@37241
   137
wenzelm@37241
   138
  def extend_styles()
wenzelm@37241
   139
  {
wenzelm@38223
   140
    Swing_Thread.require()
wenzelm@38158
   141
    styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
wenzelm@37241
   142
  }
wenzelm@37241
   143
  extend_styles()
wenzelm@37241
   144
wenzelm@37241
   145
  def set_styles()
wenzelm@37241
   146
  {
wenzelm@38223
   147
    Swing_Thread.require()
wenzelm@37241
   148
    text_area.getPainter.setStyles(styles)
wenzelm@37241
   149
  }
wenzelm@37241
   150
wenzelm@37241
   151
wenzelm@38881
   152
  /* visible line ranges */
wenzelm@38881
   153
wenzelm@38883
   154
  // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
wenzelm@38881
   155
  // NB: jEdit already normalizes \r\n and \r to \n
wenzelm@38881
   156
  def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
wenzelm@38881
   157
  {
wenzelm@38883
   158
    val stop = if (start < end) end - 1 else end min model.buffer.getLength
wenzelm@38881
   159
    Text.Range(start, stop)
wenzelm@38881
   160
  }
wenzelm@38881
   161
wenzelm@38881
   162
  def screen_lines_range(): Text.Range =
wenzelm@38881
   163
  {
wenzelm@38881
   164
    val start = text_area.getScreenLineStartOffset(0)
wenzelm@38881
   165
    val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
wenzelm@38881
   166
    proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
wenzelm@38881
   167
  }
wenzelm@38881
   168
wenzelm@39132
   169
  def invalidate_line_range(range: Text.Range)
wenzelm@39132
   170
  {
wenzelm@39132
   171
    text_area.invalidateLineRange(
wenzelm@39132
   172
      model.buffer.getLineOfOffset(range.start),
wenzelm@39132
   173
      model.buffer.getLineOfOffset(range.stop))
wenzelm@39132
   174
  }
wenzelm@39132
   175
wenzelm@38881
   176
wenzelm@37129
   177
  /* commands_changed_actor */
wenzelm@34834
   178
wenzelm@37129
   179
  private val commands_changed_actor = actor {
wenzelm@34784
   180
    loop {
wenzelm@34784
   181
      react {
wenzelm@38360
   182
        case Session.Commands_Changed(changed) =>
wenzelm@38843
   183
          val buffer = model.buffer
wenzelm@38843
   184
          Isabelle.swing_buffer_lock(buffer) {
wenzelm@38151
   185
            val snapshot = model.snapshot()
wenzelm@38881
   186
wenzelm@38884
   187
            if (changed.exists(snapshot.node.commands.contains))
wenzelm@38884
   188
              overview.repaint()
wenzelm@38884
   189
wenzelm@38881
   190
            val visible_range = screen_lines_range()
wenzelm@38881
   191
            val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
wenzelm@38881
   192
            if (visible_cmds.exists(changed)) {
wenzelm@38881
   193
              for {
wenzelm@38881
   194
                line <- 0 until text_area.getVisibleLines
wenzelm@38881
   195
                val start = text_area.getScreenLineStartOffset(line) if start >= 0
wenzelm@38881
   196
                val end = text_area.getScreenLineEndOffset(line) if end >= 0
wenzelm@38881
   197
                val range = proper_line_range(start, end)
wenzelm@38881
   198
                val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
wenzelm@38881
   199
                if line_cmds.exists(changed)
wenzelm@38881
   200
              } text_area.invalidateScreenLineRange(line, line)
wenzelm@38884
   201
wenzelm@38843
   202
              // FIXME danger of deadlock!?
wenzelm@38881
   203
              // FIXME potentially slow!?
wenzelm@38881
   204
              model.buffer.propertiesChanged()
wenzelm@38640
   205
            }
wenzelm@34834
   206
          }
wenzelm@34784
   207
wenzelm@34784
   208
        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
wenzelm@34784
   209
      }
immler@34403
   210
    }
immler@34678
   211
  }
immler@34403
   212
immler@34403
   213
wenzelm@39131
   214
  /* subexpression highlighting */
wenzelm@39131
   215
wenzelm@39174
   216
  private val subexp_include =
wenzelm@39174
   217
    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
wenzelm@39174
   218
wenzelm@39132
   219
  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
wenzelm@39132
   220
  {
wenzelm@39132
   221
    val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
wenzelm@39132
   222
    {
wenzelm@39174
   223
      case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
wenzelm@39132
   224
        Some(snapshot.convert(range))
wenzelm@39132
   225
    }
wenzelm@39132
   226
    val offset = text_area.xyToOffset(x, y)
wenzelm@39132
   227
    val markup = snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
wenzelm@39132
   228
    if (markup.hasNext) markup.next.info else None
wenzelm@39132
   229
  }
wenzelm@39132
   230
wenzelm@39132
   231
  private var highlight_range: Option[Text.Range] = None
wenzelm@39131
   232
wenzelm@39131
   233
  private val focus_listener = new FocusAdapter {
wenzelm@39132
   234
    override def focusLost(e: FocusEvent) { highlight_range = None }
wenzelm@39131
   235
  }
wenzelm@39131
   236
wenzelm@39131
   237
  private val mouse_motion_listener = new MouseMotionAdapter {
wenzelm@39131
   238
    override def mouseMoved(e: MouseEvent) {
wenzelm@39131
   239
      val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
wenzelm@39132
   240
      if (!model.buffer.isLoaded) highlight_range = None
wenzelm@39132
   241
      else
wenzelm@39132
   242
        Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@39132
   243
          highlight_range.map(invalidate_line_range(_))
wenzelm@39132
   244
          highlight_range =
wenzelm@39132
   245
            if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
wenzelm@39132
   246
          highlight_range.map(invalidate_line_range(_))
wenzelm@39132
   247
        }
wenzelm@39131
   248
    }
wenzelm@39131
   249
  }
wenzelm@39131
   250
wenzelm@39131
   251
wenzelm@34784
   252
  /* text_area_extension */
wenzelm@34784
   253
wenzelm@34784
   254
  private val text_area_extension = new TextAreaExtension
immler@34678
   255
  {
wenzelm@37685
   256
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@37685
   257
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@38886
   258
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@34784
   259
    {
wenzelm@38843
   260
      Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@38843
   261
        val snapshot = model.snapshot()
wenzelm@38843
   262
        val saved_color = gfx.getColor
wenzelm@39044
   263
        val ascent = text_area.getPainter.getFontMetrics.getAscent
wenzelm@39131
   264
wenzelm@38843
   265
        try {
wenzelm@38843
   266
          for (i <- 0 until physical_lines.length) {
wenzelm@38843
   267
            if (physical_lines(i) != -1) {
wenzelm@38881
   268
              val line_range = proper_line_range(start(i), end(i))
wenzelm@39044
   269
wenzelm@39171
   270
              // background color: status
wenzelm@38880
   271
              val cmds = snapshot.node.command_range(snapshot.revert(line_range))
wenzelm@39044
   272
              for {
wenzelm@39044
   273
                (command, command_start) <- cmds if !command.is_ignored
wenzelm@38880
   274
                val range = line_range.restrict(snapshot.convert(command.range + command_start))
wenzelm@39044
   275
                r <- Isabelle.gfx_range(text_area, range)
wenzelm@39169
   276
                color <- Document_View.status_color(snapshot, command)
wenzelm@39044
   277
              } {
wenzelm@39169
   278
                gfx.setColor(color)
wenzelm@39044
   279
                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@39044
   280
              }
wenzelm@39044
   281
wenzelm@39171
   282
              // background color: markup
wenzelm@39171
   283
              for {
wenzelm@39171
   284
                Text.Info(range, color) <-
wenzelm@39171
   285
                  snapshot.select_markup(line_range)(Document_View.background_markup)(null)
wenzelm@39171
   286
                if color != null
wenzelm@39171
   287
                r <- Isabelle.gfx_range(text_area, range)
wenzelm@39171
   288
              } {
wenzelm@39171
   289
                gfx.setColor(color)
wenzelm@39171
   290
                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@39171
   291
              }
wenzelm@39171
   292
wenzelm@39132
   293
              // subexpression highlighting -- potentially from other snapshot
wenzelm@39132
   294
              if (highlight_range.isDefined) {
wenzelm@39132
   295
                if (line_range.overlaps(highlight_range.get)) {
wenzelm@39132
   296
                  Isabelle.gfx_range(text_area, line_range.restrict(highlight_range.get)) match {
wenzelm@39131
   297
                    case None =>
wenzelm@39131
   298
                    case Some(r) =>
wenzelm@39131
   299
                      gfx.setColor(Color.black)
wenzelm@39131
   300
                      gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
wenzelm@39131
   301
                  }
wenzelm@39131
   302
                }
wenzelm@39131
   303
              }
wenzelm@39131
   304
wenzelm@39168
   305
              // boxed text
wenzelm@39168
   306
              for {
wenzelm@39168
   307
                Text.Info(range, color) <-
wenzelm@39168
   308
                  snapshot.select_markup(line_range)(Document_View.box_markup)(null)
wenzelm@39168
   309
                if color != null
wenzelm@39168
   310
                r <- Isabelle.gfx_range(text_area, range)
wenzelm@39168
   311
              } {
wenzelm@39168
   312
                gfx.setColor(color)
wenzelm@39168
   313
                gfx.drawRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 3)
wenzelm@39168
   314
              }
wenzelm@39168
   315
wenzelm@39044
   316
              // squiggly underline
wenzelm@39044
   317
              for {
wenzelm@39044
   318
                Text.Info(range, color) <-
wenzelm@39044
   319
                  snapshot.select_markup(line_range)(Document_View.message_markup)(null)
wenzelm@39044
   320
                if color != null
wenzelm@39044
   321
                r <- Isabelle.gfx_range(text_area, range)
wenzelm@39044
   322
              } {
wenzelm@39044
   323
                gfx.setColor(color)
wenzelm@39044
   324
                val x0 = (r.x / 2) * 2
wenzelm@39044
   325
                val y0 = r.y + ascent + 1
wenzelm@39044
   326
                for (x1 <- Range(x0, x0 + r.length, 2)) {
wenzelm@39044
   327
                  val y1 = if (x1 % 4 < 2) y0 else y0 + 1
wenzelm@39044
   328
                  gfx.drawLine(x1, y1, x1 + 1, y1)
wenzelm@38883
   329
                }
wenzelm@38843
   330
              }
wenzelm@38843
   331
            }
wenzelm@38223
   332
          }
wenzelm@38223
   333
        }
wenzelm@38843
   334
        finally { gfx.setColor(saved_color) }
wenzelm@38223
   335
      }
wenzelm@34784
   336
    }
wenzelm@34784
   337
wenzelm@34784
   338
    override def getToolTipText(x: Int, y: Int): String =
wenzelm@34784
   339
    {
wenzelm@38845
   340
      Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@38845
   341
        val snapshot = model.snapshot()
wenzelm@38845
   342
        val offset = text_area.xyToOffset(x, y)
wenzelm@38845
   343
        val markup =
wenzelm@39174
   344
          snapshot.select_markup(Text.Range(offset, offset + 1))(Document_View.tooltip_markup)(null)
wenzelm@39174
   345
        if (markup.hasNext) {
wenzelm@39174
   346
          val text = markup.next.info
wenzelm@39174
   347
          if (text == null) null
wenzelm@39174
   348
          else Isabelle.tooltip(text)
wenzelm@39174
   349
        }
wenzelm@39174
   350
        else null
wenzelm@34784
   351
      }
wenzelm@34734
   352
    }
immler@34678
   353
  }
immler@34513
   354
wenzelm@34784
   355
wenzelm@37129
   356
  /* caret handling */
wenzelm@34810
   357
wenzelm@37849
   358
  def selected_command(): Option[Command] =
wenzelm@38223
   359
  {
wenzelm@38223
   360
    Swing_Thread.require()
wenzelm@38151
   361
    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
wenzelm@38223
   362
  }
wenzelm@34810
   363
wenzelm@37849
   364
  private val caret_listener = new CaretListener {
wenzelm@37849
   365
    private val delay = Swing_Thread.delay_last(session.input_delay) {
wenzelm@37849
   366
      session.perspective.event(Session.Perspective)
wenzelm@34810
   367
    }
wenzelm@37849
   368
    override def caretUpdate(e: CaretEvent) { delay() }
wenzelm@34810
   369
  }
wenzelm@34810
   370
wenzelm@34810
   371
wenzelm@34784
   372
  /* overview of command status left of scrollbar */
wenzelm@34784
   373
wenzelm@34834
   374
  private val overview = new JPanel(new BorderLayout)
wenzelm@34784
   375
  {
wenzelm@34784
   376
    private val WIDTH = 10
wenzelm@34784
   377
    private val HEIGHT = 2
wenzelm@34784
   378
wenzelm@34806
   379
    setPreferredSize(new Dimension(WIDTH, 0))
wenzelm@34806
   380
wenzelm@34784
   381
    setRequestFocusEnabled(false)
wenzelm@34784
   382
wenzelm@34784
   383
    addMouseListener(new MouseAdapter {
wenzelm@34784
   384
      override def mousePressed(event: MouseEvent) {
wenzelm@34784
   385
        val line = y_to_line(event.getY)
wenzelm@34784
   386
        if (line >= 0 && line < text_area.getLineCount)
wenzelm@34784
   387
          text_area.setCaretPosition(text_area.getLineStartOffset(line))
wenzelm@34784
   388
      }
wenzelm@34784
   389
    })
wenzelm@34784
   390
wenzelm@34784
   391
    override def addNotify() {
wenzelm@34784
   392
      super.addNotify()
wenzelm@34784
   393
      ToolTipManager.sharedInstance.registerComponent(this)
wenzelm@34784
   394
    }
immler@34403
   395
wenzelm@34784
   396
    override def removeNotify() {
wenzelm@34784
   397
      ToolTipManager.sharedInstance.unregisterComponent(this)
wenzelm@34784
   398
      super.removeNotify
wenzelm@34784
   399
    }
wenzelm@34784
   400
wenzelm@34784
   401
    override def getToolTipText(event: MouseEvent): String =
wenzelm@34784
   402
    {
wenzelm@34784
   403
      val line = y_to_line(event.getY())
wenzelm@34784
   404
      if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
wenzelm@34784
   405
      else ""
wenzelm@34784
   406
    }
wenzelm@34784
   407
wenzelm@34784
   408
    override def paintComponent(gfx: Graphics)
wenzelm@34784
   409
    {
wenzelm@34784
   410
      super.paintComponent(gfx)
wenzelm@38640
   411
      Swing_Thread.assert()
wenzelm@34784
   412
      val buffer = model.buffer
wenzelm@38843
   413
      Isabelle.buffer_lock(buffer) {
wenzelm@38640
   414
        val snapshot = model.snapshot()
wenzelm@38640
   415
        val saved_color = gfx.getColor  // FIXME needed!?
wenzelm@38640
   416
        try {
wenzelm@39169
   417
          for {
wenzelm@39169
   418
            (command, start) <- snapshot.node.command_starts
wenzelm@39169
   419
            if !command.is_ignored
wenzelm@38640
   420
            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
wenzelm@38640
   421
            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
wenzelm@38640
   422
            val y = line_to_y(line1)
wenzelm@38640
   423
            val height = HEIGHT * (line2 - line1)
wenzelm@39169
   424
            color <- Document_View.overview_color(snapshot, command)
wenzelm@39169
   425
          } {
wenzelm@39169
   426
            gfx.setColor(color)
wenzelm@38640
   427
            gfx.fillRect(0, y, getWidth - 1, height)
wenzelm@38640
   428
          }
wenzelm@37188
   429
        }
wenzelm@38640
   430
        finally { gfx.setColor(saved_color) }
wenzelm@34784
   431
      }
wenzelm@34784
   432
    }
wenzelm@34784
   433
wenzelm@34784
   434
    private def line_to_y(line: Int): Int =
wenzelm@34784
   435
      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
wenzelm@34784
   436
wenzelm@34784
   437
    private def y_to_line(y: Int): Int =
wenzelm@34784
   438
      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
wenzelm@34784
   439
  }
immler@34403
   440
wenzelm@34784
   441
wenzelm@34784
   442
  /* activation */
wenzelm@34784
   443
wenzelm@34808
   444
  private def activate()
wenzelm@34784
   445
  {
wenzelm@34784
   446
    text_area.getPainter.
wenzelm@34784
   447
      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
wenzelm@39131
   448
    text_area.addFocusListener(focus_listener)
wenzelm@39131
   449
    text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
wenzelm@34810
   450
    text_area.addCaretListener(caret_listener)
wenzelm@34810
   451
    text_area.addLeftOfScrollBar(overview)
wenzelm@37129
   452
    session.commands_changed += commands_changed_actor
wenzelm@34784
   453
  }
wenzelm@34784
   454
wenzelm@34808
   455
  private def deactivate()
wenzelm@34784
   456
  {
wenzelm@37129
   457
    session.commands_changed -= commands_changed_actor
wenzelm@39131
   458
    text_area.removeFocusListener(focus_listener)
wenzelm@39131
   459
    text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
wenzelm@39131
   460
    text_area.removeCaretListener(caret_listener)
wenzelm@34810
   461
    text_area.removeLeftOfScrollBar(overview)
wenzelm@34784
   462
    text_area.getPainter.removeExtension(text_area_extension)
wenzelm@34784
   463
  }
immler@34403
   464
}