src/Tools/jEdit/src/jedit/document_view.scala
author wenzelm
Sat Aug 07 16:15:52 2010 +0200 (2010-08-07)
changeset 38223 2a368e8e0a80
parent 38158 8aaa21db41f3
child 38227 6bbb42843b6e
permissions -rw-r--r--
more explicit treatment of Swing thread context;
Document_Model.snapshot: require Swing thread;
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@34784
    15
import java.awt.event.{MouseAdapter, MouseEvent}
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@34709
    20
import org.gjt.sp.jedit.gui.RolloverButton
wenzelm@34784
    21
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
wenzelm@37241
    22
import org.gjt.sp.jedit.syntax.SyntaxStyle
wenzelm@34784
    23
wenzelm@34784
    24
wenzelm@34784
    25
object Document_View
wenzelm@34784
    26
{
wenzelm@38151
    27
  def choose_color(snapshot: Change.Snapshot, command: Command): Color =
wenzelm@34784
    28
  {
wenzelm@38151
    29
    val state = snapshot.document.current_state(command)
wenzelm@38151
    30
    if (snapshot.is_outdated) new Color(240, 240, 240)
wenzelm@38151
    31
    else if (state.forks > 0) new Color(255, 228, 225)
wenzelm@37186
    32
    else if (state.forks < 0) Color.red
wenzelm@37186
    33
    else
wenzelm@37186
    34
      state.status match {
wenzelm@37186
    35
        case Command.Status.UNPROCESSED => new Color(255, 228, 225)
wenzelm@37186
    36
        case Command.Status.FINISHED => new Color(234, 248, 255)
wenzelm@37186
    37
        case Command.Status.FAILED => new Color(255, 193, 193)
wenzelm@37186
    38
        case Command.Status.UNDEFINED => Color.red
wenzelm@37186
    39
      }
wenzelm@34784
    40
  }
wenzelm@34784
    41
wenzelm@34784
    42
wenzelm@34784
    43
  /* document view of text area */
wenzelm@34784
    44
wenzelm@34784
    45
  private val key = new Object
wenzelm@34784
    46
wenzelm@34784
    47
  def init(model: Document_Model, text_area: TextArea): Document_View =
wenzelm@34784
    48
  {
wenzelm@38223
    49
    Swing_Thread.require()
wenzelm@34784
    50
    val doc_view = new Document_View(model, text_area)
wenzelm@34784
    51
    text_area.putClientProperty(key, doc_view)
wenzelm@34784
    52
    doc_view.activate()
wenzelm@34784
    53
    doc_view
wenzelm@34784
    54
  }
wenzelm@34784
    55
wenzelm@34788
    56
  def apply(text_area: TextArea): Option[Document_View] =
wenzelm@34784
    57
  {
wenzelm@38223
    58
    Swing_Thread.require()
wenzelm@34784
    59
    text_area.getClientProperty(key) match {
wenzelm@34784
    60
      case doc_view: Document_View => Some(doc_view)
wenzelm@34784
    61
      case _ => None
wenzelm@34784
    62
    }
wenzelm@34784
    63
  }
wenzelm@34784
    64
wenzelm@34784
    65
  def exit(text_area: TextArea)
wenzelm@34784
    66
  {
wenzelm@38223
    67
    Swing_Thread.require()
wenzelm@34788
    68
    apply(text_area) match {
wenzelm@34784
    69
      case None => error("No document view for text area: " + text_area)
wenzelm@34784
    70
      case Some(doc_view) =>
wenzelm@34784
    71
        doc_view.deactivate()
wenzelm@34784
    72
        text_area.putClientProperty(key, null)
wenzelm@34784
    73
    }
wenzelm@34784
    74
  }
wenzelm@34784
    75
}
immler@34403
    76
wenzelm@34733
    77
wenzelm@37129
    78
class Document_View(val model: Document_Model, text_area: TextArea)
immler@34654
    79
{
wenzelm@34784
    80
  private val session = model.session
wenzelm@34784
    81
immler@34403
    82
wenzelm@37241
    83
  /* extended token styles */
wenzelm@37241
    84
wenzelm@37241
    85
  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
wenzelm@37241
    86
wenzelm@37241
    87
  def extend_styles()
wenzelm@37241
    88
  {
wenzelm@38223
    89
    Swing_Thread.require()
wenzelm@38158
    90
    styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
wenzelm@37241
    91
  }
wenzelm@37241
    92
  extend_styles()
wenzelm@37241
    93
wenzelm@37241
    94
  def set_styles()
wenzelm@37241
    95
  {
wenzelm@38223
    96
    Swing_Thread.require()
wenzelm@37241
    97
    text_area.getPainter.setStyles(styles)
wenzelm@37241
    98
  }
wenzelm@37241
    99
wenzelm@37241
   100
wenzelm@37129
   101
  /* commands_changed_actor */
wenzelm@34834
   102
wenzelm@37129
   103
  private val commands_changed_actor = actor {
wenzelm@34784
   104
    loop {
wenzelm@34784
   105
      react {
wenzelm@37129
   106
        case Command_Set(changed) =>
wenzelm@34834
   107
          Swing_Thread.now {
wenzelm@37685
   108
            // FIXME cover doc states as well!!?
wenzelm@38151
   109
            val snapshot = model.snapshot()
wenzelm@38151
   110
            if (changed.exists(snapshot.node.commands.contains))
wenzelm@38151
   111
              full_repaint(snapshot, changed)
wenzelm@34834
   112
          }
wenzelm@34784
   113
wenzelm@34784
   114
        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
wenzelm@34784
   115
      }
immler@34403
   116
    }
immler@34678
   117
  }
immler@34403
   118
wenzelm@38151
   119
  def full_repaint(snapshot: Change.Snapshot, changed: Set[Command])
wenzelm@37685
   120
  {
wenzelm@38223
   121
    Swing_Thread.require()
wenzelm@37685
   122
wenzelm@37685
   123
    val buffer = model.buffer
wenzelm@37685
   124
    var visible_change = false
wenzelm@37685
   125
wenzelm@38152
   126
    for ((command, start) <- snapshot.node.command_starts) {
wenzelm@37685
   127
      if (changed(command)) {
wenzelm@37685
   128
        val stop = start + command.length
wenzelm@38153
   129
        val line1 = buffer.getLineOfOffset(snapshot.convert(start))
wenzelm@38153
   130
        val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
wenzelm@37685
   131
        if (line2 >= text_area.getFirstLine &&
wenzelm@37685
   132
            line1 <= text_area.getFirstLine + text_area.getVisibleLines)
wenzelm@37685
   133
          visible_change = true
wenzelm@37685
   134
        text_area.invalidateLineRange(line1, line2)
wenzelm@37685
   135
      }
wenzelm@37685
   136
    }
wenzelm@37685
   137
    if (visible_change) model.buffer.propertiesChanged()
wenzelm@37685
   138
wenzelm@37685
   139
    overview.repaint()  // FIXME paint here!?
wenzelm@37685
   140
  }
wenzelm@37685
   141
immler@34403
   142
wenzelm@34784
   143
  /* text_area_extension */
wenzelm@34784
   144
wenzelm@34784
   145
  private val text_area_extension = new TextAreaExtension
immler@34678
   146
  {
wenzelm@37685
   147
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@37685
   148
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@37685
   149
      start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
wenzelm@34784
   150
    {
wenzelm@38223
   151
      Swing_Thread.assert()
wenzelm@38223
   152
wenzelm@38223
   153
      val snapshot = model.snapshot()
wenzelm@38223
   154
wenzelm@38223
   155
      val command_range: Iterable[(Command, Int)] =
wenzelm@38223
   156
      {
wenzelm@38223
   157
        val range = snapshot.node.command_range(snapshot.revert(start(0)))
wenzelm@38223
   158
        if (range.hasNext) {
wenzelm@38223
   159
          val (cmd0, start0) = range.next
wenzelm@38223
   160
          new Iterable[(Command, Int)] {
wenzelm@38223
   161
            def iterator = Document.command_starts(snapshot.node.commands.iterator(cmd0), start0)
wenzelm@38223
   162
          }
wenzelm@38223
   163
        }
wenzelm@38223
   164
        else Iterable.empty
wenzelm@38223
   165
      }
wenzelm@37555
   166
wenzelm@38223
   167
      val saved_color = gfx.getColor
wenzelm@38223
   168
      try {
wenzelm@38223
   169
        var y = y0
wenzelm@38223
   170
        for (i <- 0 until physical_lines.length) {
wenzelm@38223
   171
          if (physical_lines(i) != -1) {
wenzelm@38223
   172
            val line_start = start(i)
wenzelm@38223
   173
            val line_end = model.visible_line_end(line_start, end(i))
wenzelm@38223
   174
wenzelm@38223
   175
            val a = snapshot.revert(line_start)
wenzelm@38223
   176
            val b = snapshot.revert(line_end)
wenzelm@38223
   177
            val cmds = command_range.iterator.
wenzelm@38223
   178
              dropWhile { case (cmd, c) => c + cmd.length <= a } .
wenzelm@38223
   179
              takeWhile { case (_, c) => c < b }
wenzelm@38223
   180
wenzelm@38223
   181
            for ((command, command_start) <- cmds if !command.is_ignored) {
wenzelm@38223
   182
              val p =
wenzelm@38223
   183
                text_area.offsetToXY(line_start max snapshot.convert(command_start))
wenzelm@38223
   184
              val q =
wenzelm@38223
   185
                text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
wenzelm@38223
   186
              assert(p.y == q.y)
wenzelm@38223
   187
              gfx.setColor(Document_View.choose_color(snapshot, command))
wenzelm@38223
   188
              gfx.fillRect(p.x, y, q.x - p.x, line_height)
wenzelm@37685
   189
            }
wenzelm@37685
   190
          }
wenzelm@38223
   191
          y += line_height
wenzelm@37685
   192
        }
wenzelm@34784
   193
      }
wenzelm@38223
   194
      finally { gfx.setColor(saved_color) }
wenzelm@34784
   195
    }
wenzelm@34784
   196
wenzelm@34784
   197
    override def getToolTipText(x: Int, y: Int): String =
wenzelm@34784
   198
    {
wenzelm@38223
   199
      Swing_Thread.assert()
wenzelm@38223
   200
wenzelm@38151
   201
      val snapshot = model.snapshot()
wenzelm@38153
   202
      val offset = snapshot.revert(text_area.xyToOffset(x, y))
wenzelm@38152
   203
      snapshot.node.command_at(offset) match {
wenzelm@34855
   204
        case Some((command, command_start)) =>
wenzelm@38152
   205
          snapshot.document.current_state(command).type_at(offset - command_start) match {
wenzelm@37201
   206
            case Some(text) => Isabelle.tooltip(text)
wenzelm@37201
   207
            case None => null
wenzelm@37201
   208
          }
wenzelm@34784
   209
        case None => null
wenzelm@34784
   210
      }
wenzelm@34734
   211
    }
immler@34678
   212
  }
immler@34513
   213
wenzelm@34784
   214
wenzelm@37129
   215
  /* caret handling */
wenzelm@34810
   216
wenzelm@37849
   217
  def selected_command(): Option[Command] =
wenzelm@38223
   218
  {
wenzelm@38223
   219
    Swing_Thread.require()
wenzelm@38151
   220
    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
wenzelm@38223
   221
  }
wenzelm@34810
   222
wenzelm@37849
   223
  private val caret_listener = new CaretListener {
wenzelm@37849
   224
    private val delay = Swing_Thread.delay_last(session.input_delay) {
wenzelm@37849
   225
      session.perspective.event(Session.Perspective)
wenzelm@34810
   226
    }
wenzelm@37849
   227
    override def caretUpdate(e: CaretEvent) { delay() }
wenzelm@34810
   228
  }
wenzelm@34810
   229
wenzelm@34810
   230
wenzelm@34784
   231
  /* overview of command status left of scrollbar */
wenzelm@34784
   232
wenzelm@34834
   233
  private val overview = new JPanel(new BorderLayout)
wenzelm@34784
   234
  {
wenzelm@34784
   235
    private val WIDTH = 10
wenzelm@34784
   236
    private val HEIGHT = 2
wenzelm@34784
   237
wenzelm@34806
   238
    setPreferredSize(new Dimension(WIDTH, 0))
wenzelm@34806
   239
wenzelm@34784
   240
    setRequestFocusEnabled(false)
wenzelm@34784
   241
wenzelm@34784
   242
    addMouseListener(new MouseAdapter {
wenzelm@34784
   243
      override def mousePressed(event: MouseEvent) {
wenzelm@34784
   244
        val line = y_to_line(event.getY)
wenzelm@34784
   245
        if (line >= 0 && line < text_area.getLineCount)
wenzelm@34784
   246
          text_area.setCaretPosition(text_area.getLineStartOffset(line))
wenzelm@34784
   247
      }
wenzelm@34784
   248
    })
wenzelm@34784
   249
wenzelm@34784
   250
    override def addNotify() {
wenzelm@34784
   251
      super.addNotify()
wenzelm@34784
   252
      ToolTipManager.sharedInstance.registerComponent(this)
wenzelm@34784
   253
    }
immler@34403
   254
wenzelm@34784
   255
    override def removeNotify() {
wenzelm@34784
   256
      ToolTipManager.sharedInstance.unregisterComponent(this)
wenzelm@34784
   257
      super.removeNotify
wenzelm@34784
   258
    }
wenzelm@34784
   259
wenzelm@34784
   260
    override def getToolTipText(event: MouseEvent): String =
wenzelm@34784
   261
    {
wenzelm@34784
   262
      val line = y_to_line(event.getY())
wenzelm@34784
   263
      if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
wenzelm@34784
   264
      else ""
wenzelm@34784
   265
    }
wenzelm@34784
   266
wenzelm@34784
   267
    override def paintComponent(gfx: Graphics)
wenzelm@34784
   268
    {
wenzelm@34784
   269
      super.paintComponent(gfx)
wenzelm@34784
   270
      val buffer = model.buffer
wenzelm@38151
   271
      val snapshot = model.snapshot()
wenzelm@37685
   272
      val saved_color = gfx.getColor  // FIXME needed!?
wenzelm@37188
   273
      try {
wenzelm@38151
   274
        for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
wenzelm@38153
   275
          val line1 = buffer.getLineOfOffset(snapshot.convert(start))
wenzelm@38153
   276
          val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
wenzelm@37188
   277
          val y = line_to_y(line1)
wenzelm@37188
   278
          val height = HEIGHT * (line2 - line1)
wenzelm@38151
   279
          gfx.setColor(Document_View.choose_color(snapshot, command))
wenzelm@37188
   280
          gfx.fillRect(0, y, getWidth - 1, height)
wenzelm@37188
   281
        }
wenzelm@34784
   282
      }
wenzelm@37188
   283
      finally { gfx.setColor(saved_color) }
wenzelm@34784
   284
    }
wenzelm@34784
   285
wenzelm@34784
   286
    private def line_to_y(line: Int): Int =
wenzelm@34784
   287
      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
wenzelm@34784
   288
wenzelm@34784
   289
    private def y_to_line(y: Int): Int =
wenzelm@34784
   290
      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
wenzelm@34784
   291
  }
immler@34403
   292
wenzelm@34784
   293
wenzelm@34784
   294
  /* activation */
wenzelm@34784
   295
wenzelm@34808
   296
  private def activate()
wenzelm@34784
   297
  {
wenzelm@34784
   298
    text_area.getPainter.
wenzelm@34784
   299
      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
wenzelm@34810
   300
    text_area.addCaretListener(caret_listener)
wenzelm@34810
   301
    text_area.addLeftOfScrollBar(overview)
wenzelm@37129
   302
    session.commands_changed += commands_changed_actor
wenzelm@34784
   303
  }
wenzelm@34784
   304
wenzelm@34808
   305
  private def deactivate()
wenzelm@34784
   306
  {
wenzelm@37129
   307
    session.commands_changed -= commands_changed_actor
wenzelm@34810
   308
    text_area.removeLeftOfScrollBar(overview)
wenzelm@34810
   309
    text_area.removeCaretListener(caret_listener)
wenzelm@34784
   310
    text_area.getPainter.removeExtension(text_area_extension)
wenzelm@34784
   311
  }
immler@34403
   312
}