src/Tools/jEdit/src/jedit/document_view.scala
author wenzelm
Tue Aug 31 17:49:45 2010 +0200 (2010-08-31)
changeset 38884 9ec5f6010d6e
parent 38883 0998a635684a
child 38886 9210cf2b4869
permissions -rw-r--r--
Document_View: repaint overview for any command change of this node (again);
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@37186
    31
    else
wenzelm@38567
    32
      Isar_Document.command_status(state.status) match {
wenzelm@38567
    33
        case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
wenzelm@38567
    34
        case Isar_Document.Finished => new Color(234, 248, 255)
wenzelm@38567
    35
        case Isar_Document.Failed => new Color(255, 193, 193)
wenzelm@38567
    36
        case Isar_Document.Unprocessed => new Color(255, 228, 225)
wenzelm@38429
    37
        case _ => Color.red
wenzelm@37186
    38
      }
wenzelm@34784
    39
  }
wenzelm@34784
    40
wenzelm@34784
    41
wenzelm@34784
    42
  /* document view of text area */
wenzelm@34784
    43
wenzelm@34784
    44
  private val key = new Object
wenzelm@34784
    45
wenzelm@34784
    46
  def init(model: Document_Model, text_area: TextArea): Document_View =
wenzelm@34784
    47
  {
wenzelm@38223
    48
    Swing_Thread.require()
wenzelm@34784
    49
    val doc_view = new Document_View(model, text_area)
wenzelm@34784
    50
    text_area.putClientProperty(key, doc_view)
wenzelm@34784
    51
    doc_view.activate()
wenzelm@34784
    52
    doc_view
wenzelm@34784
    53
  }
wenzelm@34784
    54
wenzelm@34788
    55
  def apply(text_area: TextArea): Option[Document_View] =
wenzelm@34784
    56
  {
wenzelm@38223
    57
    Swing_Thread.require()
wenzelm@34784
    58
    text_area.getClientProperty(key) match {
wenzelm@34784
    59
      case doc_view: Document_View => Some(doc_view)
wenzelm@34784
    60
      case _ => None
wenzelm@34784
    61
    }
wenzelm@34784
    62
  }
wenzelm@34784
    63
wenzelm@34784
    64
  def exit(text_area: TextArea)
wenzelm@34784
    65
  {
wenzelm@38223
    66
    Swing_Thread.require()
wenzelm@34788
    67
    apply(text_area) match {
wenzelm@34784
    68
      case None => error("No document view for text area: " + text_area)
wenzelm@34784
    69
      case Some(doc_view) =>
wenzelm@34784
    70
        doc_view.deactivate()
wenzelm@34784
    71
        text_area.putClientProperty(key, null)
wenzelm@34784
    72
    }
wenzelm@34784
    73
  }
wenzelm@34784
    74
}
immler@34403
    75
wenzelm@34733
    76
wenzelm@37129
    77
class Document_View(val model: Document_Model, text_area: TextArea)
immler@34654
    78
{
wenzelm@34784
    79
  private val session = model.session
wenzelm@34784
    80
immler@34403
    81
wenzelm@37241
    82
  /* extended token styles */
wenzelm@37241
    83
wenzelm@37241
    84
  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
wenzelm@37241
    85
wenzelm@37241
    86
  def extend_styles()
wenzelm@37241
    87
  {
wenzelm@38223
    88
    Swing_Thread.require()
wenzelm@38158
    89
    styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
wenzelm@37241
    90
  }
wenzelm@37241
    91
  extend_styles()
wenzelm@37241
    92
wenzelm@37241
    93
  def set_styles()
wenzelm@37241
    94
  {
wenzelm@38223
    95
    Swing_Thread.require()
wenzelm@37241
    96
    text_area.getPainter.setStyles(styles)
wenzelm@37241
    97
  }
wenzelm@37241
    98
wenzelm@37241
    99
wenzelm@38881
   100
  /* visible line ranges */
wenzelm@38881
   101
wenzelm@38883
   102
  // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
wenzelm@38881
   103
  // NB: jEdit already normalizes \r\n and \r to \n
wenzelm@38881
   104
  def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
wenzelm@38881
   105
  {
wenzelm@38883
   106
    val stop = if (start < end) end - 1 else end min model.buffer.getLength
wenzelm@38881
   107
    Text.Range(start, stop)
wenzelm@38881
   108
  }
wenzelm@38881
   109
wenzelm@38881
   110
  def screen_lines_range(): Text.Range =
wenzelm@38881
   111
  {
wenzelm@38881
   112
    val start = text_area.getScreenLineStartOffset(0)
wenzelm@38881
   113
    val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
wenzelm@38881
   114
    proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
wenzelm@38881
   115
  }
wenzelm@38881
   116
wenzelm@38881
   117
wenzelm@37129
   118
  /* commands_changed_actor */
wenzelm@34834
   119
wenzelm@37129
   120
  private val commands_changed_actor = actor {
wenzelm@34784
   121
    loop {
wenzelm@34784
   122
      react {
wenzelm@38360
   123
        case Session.Commands_Changed(changed) =>
wenzelm@38843
   124
          val buffer = model.buffer
wenzelm@38843
   125
          Isabelle.swing_buffer_lock(buffer) {
wenzelm@38151
   126
            val snapshot = model.snapshot()
wenzelm@38881
   127
wenzelm@38884
   128
            if (changed.exists(snapshot.node.commands.contains))
wenzelm@38884
   129
              overview.repaint()
wenzelm@38884
   130
wenzelm@38881
   131
            val visible_range = screen_lines_range()
wenzelm@38881
   132
            val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
wenzelm@38881
   133
            if (visible_cmds.exists(changed)) {
wenzelm@38881
   134
              for {
wenzelm@38881
   135
                line <- 0 until text_area.getVisibleLines
wenzelm@38881
   136
                val start = text_area.getScreenLineStartOffset(line) if start >= 0
wenzelm@38881
   137
                val end = text_area.getScreenLineEndOffset(line) if end >= 0
wenzelm@38881
   138
                val range = proper_line_range(start, end)
wenzelm@38881
   139
                val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
wenzelm@38881
   140
                if line_cmds.exists(changed)
wenzelm@38881
   141
              } text_area.invalidateScreenLineRange(line, line)
wenzelm@38884
   142
wenzelm@38843
   143
              // FIXME danger of deadlock!?
wenzelm@38881
   144
              // FIXME potentially slow!?
wenzelm@38881
   145
              model.buffer.propertiesChanged()
wenzelm@38640
   146
            }
wenzelm@34834
   147
          }
wenzelm@34784
   148
wenzelm@34784
   149
        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
wenzelm@34784
   150
      }
immler@34403
   151
    }
immler@34678
   152
  }
immler@34403
   153
immler@34403
   154
wenzelm@34784
   155
  /* text_area_extension */
wenzelm@34784
   156
wenzelm@34784
   157
  private val text_area_extension = new TextAreaExtension
immler@34678
   158
  {
wenzelm@37685
   159
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@37685
   160
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@37685
   161
      start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
wenzelm@34784
   162
    {
wenzelm@38843
   163
      Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@38843
   164
        val snapshot = model.snapshot()
wenzelm@38843
   165
        val saved_color = gfx.getColor
wenzelm@38843
   166
        try {
wenzelm@38843
   167
          var y = y0
wenzelm@38843
   168
          for (i <- 0 until physical_lines.length) {
wenzelm@38843
   169
            if (physical_lines(i) != -1) {
wenzelm@38881
   170
              val line_range = proper_line_range(start(i), end(i))
wenzelm@38880
   171
              val cmds = snapshot.node.command_range(snapshot.revert(line_range))
wenzelm@38843
   172
              for ((command, command_start) <- cmds if !command.is_ignored) {
wenzelm@38880
   173
                val range = line_range.restrict(snapshot.convert(command.range + command_start))
wenzelm@38880
   174
                val p = text_area.offsetToXY(range.start)
wenzelm@38880
   175
                val q = text_area.offsetToXY(range.stop)
wenzelm@38883
   176
                if (p != null && q != null) {
wenzelm@38883
   177
                  gfx.setColor(Document_View.choose_color(snapshot, command))
wenzelm@38883
   178
                  gfx.fillRect(p.x, y, q.x - p.x, line_height)
wenzelm@38883
   179
                }
wenzelm@38843
   180
              }
wenzelm@38843
   181
            }
wenzelm@38843
   182
            y += line_height
wenzelm@38223
   183
          }
wenzelm@38223
   184
        }
wenzelm@38843
   185
        finally { gfx.setColor(saved_color) }
wenzelm@38223
   186
      }
wenzelm@34784
   187
    }
wenzelm@34784
   188
wenzelm@34784
   189
    override def getToolTipText(x: Int, y: Int): String =
wenzelm@34784
   190
    {
wenzelm@38845
   191
      Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@38845
   192
        val snapshot = model.snapshot()
wenzelm@38845
   193
        val offset = text_area.xyToOffset(x, y)
wenzelm@38845
   194
        val markup =
wenzelm@38845
   195
          snapshot.select_markup(Text.Range(offset, offset + 1)) {
wenzelm@38580
   196
            case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
wenzelm@38845
   197
              Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40))
wenzelm@38845
   198
          } { null }
wenzelm@38845
   199
        if (markup.hasNext) markup.next.info else null
wenzelm@34784
   200
      }
wenzelm@34734
   201
    }
immler@34678
   202
  }
immler@34513
   203
wenzelm@34784
   204
wenzelm@37129
   205
  /* caret handling */
wenzelm@34810
   206
wenzelm@37849
   207
  def selected_command(): Option[Command] =
wenzelm@38223
   208
  {
wenzelm@38223
   209
    Swing_Thread.require()
wenzelm@38151
   210
    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
wenzelm@38223
   211
  }
wenzelm@34810
   212
wenzelm@37849
   213
  private val caret_listener = new CaretListener {
wenzelm@37849
   214
    private val delay = Swing_Thread.delay_last(session.input_delay) {
wenzelm@37849
   215
      session.perspective.event(Session.Perspective)
wenzelm@34810
   216
    }
wenzelm@37849
   217
    override def caretUpdate(e: CaretEvent) { delay() }
wenzelm@34810
   218
  }
wenzelm@34810
   219
wenzelm@34810
   220
wenzelm@34784
   221
  /* overview of command status left of scrollbar */
wenzelm@34784
   222
wenzelm@34834
   223
  private val overview = new JPanel(new BorderLayout)
wenzelm@34784
   224
  {
wenzelm@34784
   225
    private val WIDTH = 10
wenzelm@34784
   226
    private val HEIGHT = 2
wenzelm@34784
   227
wenzelm@34806
   228
    setPreferredSize(new Dimension(WIDTH, 0))
wenzelm@34806
   229
wenzelm@34784
   230
    setRequestFocusEnabled(false)
wenzelm@34784
   231
wenzelm@34784
   232
    addMouseListener(new MouseAdapter {
wenzelm@34784
   233
      override def mousePressed(event: MouseEvent) {
wenzelm@34784
   234
        val line = y_to_line(event.getY)
wenzelm@34784
   235
        if (line >= 0 && line < text_area.getLineCount)
wenzelm@34784
   236
          text_area.setCaretPosition(text_area.getLineStartOffset(line))
wenzelm@34784
   237
      }
wenzelm@34784
   238
    })
wenzelm@34784
   239
wenzelm@34784
   240
    override def addNotify() {
wenzelm@34784
   241
      super.addNotify()
wenzelm@34784
   242
      ToolTipManager.sharedInstance.registerComponent(this)
wenzelm@34784
   243
    }
immler@34403
   244
wenzelm@34784
   245
    override def removeNotify() {
wenzelm@34784
   246
      ToolTipManager.sharedInstance.unregisterComponent(this)
wenzelm@34784
   247
      super.removeNotify
wenzelm@34784
   248
    }
wenzelm@34784
   249
wenzelm@34784
   250
    override def getToolTipText(event: MouseEvent): String =
wenzelm@34784
   251
    {
wenzelm@34784
   252
      val line = y_to_line(event.getY())
wenzelm@34784
   253
      if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
wenzelm@34784
   254
      else ""
wenzelm@34784
   255
    }
wenzelm@34784
   256
wenzelm@34784
   257
    override def paintComponent(gfx: Graphics)
wenzelm@34784
   258
    {
wenzelm@34784
   259
      super.paintComponent(gfx)
wenzelm@38640
   260
      Swing_Thread.assert()
wenzelm@34784
   261
      val buffer = model.buffer
wenzelm@38843
   262
      Isabelle.buffer_lock(buffer) {
wenzelm@38640
   263
        val snapshot = model.snapshot()
wenzelm@38640
   264
        val saved_color = gfx.getColor  // FIXME needed!?
wenzelm@38640
   265
        try {
wenzelm@38640
   266
          for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
wenzelm@38640
   267
            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
wenzelm@38640
   268
            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
wenzelm@38640
   269
            val y = line_to_y(line1)
wenzelm@38640
   270
            val height = HEIGHT * (line2 - line1)
wenzelm@38640
   271
            gfx.setColor(Document_View.choose_color(snapshot, command))
wenzelm@38640
   272
            gfx.fillRect(0, y, getWidth - 1, height)
wenzelm@38640
   273
          }
wenzelm@37188
   274
        }
wenzelm@38640
   275
        finally { gfx.setColor(saved_color) }
wenzelm@34784
   276
      }
wenzelm@34784
   277
    }
wenzelm@34784
   278
wenzelm@34784
   279
    private def line_to_y(line: Int): Int =
wenzelm@34784
   280
      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
wenzelm@34784
   281
wenzelm@34784
   282
    private def y_to_line(y: Int): Int =
wenzelm@34784
   283
      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
wenzelm@34784
   284
  }
immler@34403
   285
wenzelm@34784
   286
wenzelm@34784
   287
  /* activation */
wenzelm@34784
   288
wenzelm@34808
   289
  private def activate()
wenzelm@34784
   290
  {
wenzelm@34784
   291
    text_area.getPainter.
wenzelm@34784
   292
      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
wenzelm@34810
   293
    text_area.addCaretListener(caret_listener)
wenzelm@34810
   294
    text_area.addLeftOfScrollBar(overview)
wenzelm@37129
   295
    session.commands_changed += commands_changed_actor
wenzelm@34784
   296
  }
wenzelm@34784
   297
wenzelm@34808
   298
  private def deactivate()
wenzelm@34784
   299
  {
wenzelm@37129
   300
    session.commands_changed -= commands_changed_actor
wenzelm@34810
   301
    text_area.removeLeftOfScrollBar(overview)
wenzelm@34810
   302
    text_area.removeCaretListener(caret_listener)
wenzelm@34784
   303
    text_area.getPainter.removeExtension(text_area_extension)
wenzelm@34784
   304
  }
immler@34403
   305
}