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