src/Tools/jEdit/src/jedit/document_view.scala
author wenzelm
Sun Aug 15 22:48:56 2010 +0200 (2010-08-15)
changeset 38426 2858ec7b6dd8
parent 38360 53224a4d2f0e
child 38429 9951852fae91
permissions -rw-r--r--
specific types Text.Offset and Text.Range;
minor tuning;
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@38227
    27
  def choose_color(snapshot: Document.Snapshot, command: Command): Color =
wenzelm@34784
    28
  {
wenzelm@38356
    29
    val state = snapshot.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@38360
   106
        case Session.Commands_Changed(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@38227
   119
  def full_repaint(snapshot: Document.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@38426
   155
      val command_range: Iterable[(Command, Text.Offset)] =
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@38426
   160
          new Iterable[(Command, Text.Offset)] {
wenzelm@38227
   161
            def iterator =
wenzelm@38227
   162
              Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
wenzelm@38223
   163
          }
wenzelm@38223
   164
        }
wenzelm@38223
   165
        else Iterable.empty
wenzelm@38223
   166
      }
wenzelm@37555
   167
wenzelm@38223
   168
      val saved_color = gfx.getColor
wenzelm@38223
   169
      try {
wenzelm@38223
   170
        var y = y0
wenzelm@38223
   171
        for (i <- 0 until physical_lines.length) {
wenzelm@38223
   172
          if (physical_lines(i) != -1) {
wenzelm@38223
   173
            val line_start = start(i)
wenzelm@38223
   174
            val line_end = model.visible_line_end(line_start, end(i))
wenzelm@38223
   175
wenzelm@38223
   176
            val a = snapshot.revert(line_start)
wenzelm@38223
   177
            val b = snapshot.revert(line_end)
wenzelm@38223
   178
            val cmds = command_range.iterator.
wenzelm@38223
   179
              dropWhile { case (cmd, c) => c + cmd.length <= a } .
wenzelm@38223
   180
              takeWhile { case (_, c) => c < b }
wenzelm@38223
   181
wenzelm@38223
   182
            for ((command, command_start) <- cmds if !command.is_ignored) {
wenzelm@38223
   183
              val p =
wenzelm@38223
   184
                text_area.offsetToXY(line_start max snapshot.convert(command_start))
wenzelm@38223
   185
              val q =
wenzelm@38223
   186
                text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
wenzelm@38223
   187
              assert(p.y == q.y)
wenzelm@38223
   188
              gfx.setColor(Document_View.choose_color(snapshot, command))
wenzelm@38223
   189
              gfx.fillRect(p.x, y, q.x - p.x, line_height)
wenzelm@37685
   190
            }
wenzelm@37685
   191
          }
wenzelm@38223
   192
          y += line_height
wenzelm@37685
   193
        }
wenzelm@34784
   194
      }
wenzelm@38223
   195
      finally { gfx.setColor(saved_color) }
wenzelm@34784
   196
    }
wenzelm@34784
   197
wenzelm@34784
   198
    override def getToolTipText(x: Int, y: Int): String =
wenzelm@34784
   199
    {
wenzelm@38223
   200
      Swing_Thread.assert()
wenzelm@38223
   201
wenzelm@38151
   202
      val snapshot = model.snapshot()
wenzelm@38153
   203
      val offset = snapshot.revert(text_area.xyToOffset(x, y))
wenzelm@38152
   204
      snapshot.node.command_at(offset) match {
wenzelm@34855
   205
        case Some((command, command_start)) =>
wenzelm@38356
   206
          snapshot.state(command).type_at(offset - command_start) match {
wenzelm@37201
   207
            case Some(text) => Isabelle.tooltip(text)
wenzelm@37201
   208
            case None => null
wenzelm@37201
   209
          }
wenzelm@34784
   210
        case None => null
wenzelm@34784
   211
      }
wenzelm@34734
   212
    }
immler@34678
   213
  }
immler@34513
   214
wenzelm@34784
   215
wenzelm@37129
   216
  /* caret handling */
wenzelm@34810
   217
wenzelm@37849
   218
  def selected_command(): Option[Command] =
wenzelm@38223
   219
  {
wenzelm@38223
   220
    Swing_Thread.require()
wenzelm@38151
   221
    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
wenzelm@38223
   222
  }
wenzelm@34810
   223
wenzelm@37849
   224
  private val caret_listener = new CaretListener {
wenzelm@37849
   225
    private val delay = Swing_Thread.delay_last(session.input_delay) {
wenzelm@37849
   226
      session.perspective.event(Session.Perspective)
wenzelm@34810
   227
    }
wenzelm@37849
   228
    override def caretUpdate(e: CaretEvent) { delay() }
wenzelm@34810
   229
  }
wenzelm@34810
   230
wenzelm@34810
   231
wenzelm@34784
   232
  /* overview of command status left of scrollbar */
wenzelm@34784
   233
wenzelm@34834
   234
  private val overview = new JPanel(new BorderLayout)
wenzelm@34784
   235
  {
wenzelm@34784
   236
    private val WIDTH = 10
wenzelm@34784
   237
    private val HEIGHT = 2
wenzelm@34784
   238
wenzelm@34806
   239
    setPreferredSize(new Dimension(WIDTH, 0))
wenzelm@34806
   240
wenzelm@34784
   241
    setRequestFocusEnabled(false)
wenzelm@34784
   242
wenzelm@34784
   243
    addMouseListener(new MouseAdapter {
wenzelm@34784
   244
      override def mousePressed(event: MouseEvent) {
wenzelm@34784
   245
        val line = y_to_line(event.getY)
wenzelm@34784
   246
        if (line >= 0 && line < text_area.getLineCount)
wenzelm@34784
   247
          text_area.setCaretPosition(text_area.getLineStartOffset(line))
wenzelm@34784
   248
      }
wenzelm@34784
   249
    })
wenzelm@34784
   250
wenzelm@34784
   251
    override def addNotify() {
wenzelm@34784
   252
      super.addNotify()
wenzelm@34784
   253
      ToolTipManager.sharedInstance.registerComponent(this)
wenzelm@34784
   254
    }
immler@34403
   255
wenzelm@34784
   256
    override def removeNotify() {
wenzelm@34784
   257
      ToolTipManager.sharedInstance.unregisterComponent(this)
wenzelm@34784
   258
      super.removeNotify
wenzelm@34784
   259
    }
wenzelm@34784
   260
wenzelm@34784
   261
    override def getToolTipText(event: MouseEvent): String =
wenzelm@34784
   262
    {
wenzelm@34784
   263
      val line = y_to_line(event.getY())
wenzelm@34784
   264
      if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
wenzelm@34784
   265
      else ""
wenzelm@34784
   266
    }
wenzelm@34784
   267
wenzelm@34784
   268
    override def paintComponent(gfx: Graphics)
wenzelm@34784
   269
    {
wenzelm@34784
   270
      super.paintComponent(gfx)
wenzelm@34784
   271
      val buffer = model.buffer
wenzelm@38151
   272
      val snapshot = model.snapshot()
wenzelm@37685
   273
      val saved_color = gfx.getColor  // FIXME needed!?
wenzelm@37188
   274
      try {
wenzelm@38151
   275
        for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
wenzelm@38153
   276
          val line1 = buffer.getLineOfOffset(snapshot.convert(start))
wenzelm@38153
   277
          val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
wenzelm@37188
   278
          val y = line_to_y(line1)
wenzelm@37188
   279
          val height = HEIGHT * (line2 - line1)
wenzelm@38151
   280
          gfx.setColor(Document_View.choose_color(snapshot, command))
wenzelm@37188
   281
          gfx.fillRect(0, y, getWidth - 1, height)
wenzelm@37188
   282
        }
wenzelm@34784
   283
      }
wenzelm@37188
   284
      finally { gfx.setColor(saved_color) }
wenzelm@34784
   285
    }
wenzelm@34784
   286
wenzelm@34784
   287
    private def line_to_y(line: Int): Int =
wenzelm@34784
   288
      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
wenzelm@34784
   289
wenzelm@34784
   290
    private def y_to_line(y: Int): Int =
wenzelm@34784
   291
      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
wenzelm@34784
   292
  }
immler@34403
   293
wenzelm@34784
   294
wenzelm@34784
   295
  /* activation */
wenzelm@34784
   296
wenzelm@34808
   297
  private def activate()
wenzelm@34784
   298
  {
wenzelm@34784
   299
    text_area.getPainter.
wenzelm@34784
   300
      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
wenzelm@34810
   301
    text_area.addCaretListener(caret_listener)
wenzelm@34810
   302
    text_area.addLeftOfScrollBar(overview)
wenzelm@37129
   303
    session.commands_changed += commands_changed_actor
wenzelm@34784
   304
  }
wenzelm@34784
   305
wenzelm@34808
   306
  private def deactivate()
wenzelm@34784
   307
  {
wenzelm@37129
   308
    session.commands_changed -= commands_changed_actor
wenzelm@34810
   309
    text_area.removeLeftOfScrollBar(overview)
wenzelm@34810
   310
    text_area.removeCaretListener(caret_listener)
wenzelm@34784
   311
    text_area.getPainter.removeExtension(text_area_extension)
wenzelm@34784
   312
  }
immler@34403
   313
}