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